============================== FOF-Prover9 =========================== FOF-Prover9 (32) version March-2007, March 2007. Process 20920 was started by mccune on cleo, Mon Mar 19 17:01:17 2007 The command was "/home/mccune/bin/fof-prover9 -f GEO146+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file GEO146+1.in set(prolog_style_variables). formulas(assumptions). (all C all C1 (part_of(C1,C) <-> (all P (incident_c(P,C1) -> incident_c(P,C))))). (all C all C1 all C2 (C = sum(C1,C2) <-> (all Q (incident_c(Q,C) <-> incident_c(Q,C1) | incident_c(Q,C2))))). (all P all C (end_point(P,C) <-> incident_c(P,C) & (all C1 all C2 (part_of(C1,C) & part_of(C2,C) & incident_c(P,C1) & incident_c(P,C2) -> part_of(C1,C2) | part_of(C2,C1))))). (all P all C (inner_point(P,C) <-> incident_c(P,C) & -end_point(P,C))). (all P all C all C1 (meet(P,C,C1) <-> incident_c(P,C) & incident_c(P,C1) & (all Q (incident_c(Q,C) & incident_c(Q,C1) -> end_point(Q,C) & end_point(Q,C1))))). (all C (closed(C) <-> -(exists P end_point(P,C)))). (all C (open(C) <-> (exists P end_point(P,C)))). (all C all C1 (part_of(C1,C) & C1 != C -> open(C1))). (all C all C1 all C2 all C3 (part_of(C1,C) & part_of(C2,C) & part_of(C3,C) & (exists P (end_point(P,C1) & end_point(P,C2) & end_point(P,C3))) -> part_of(C2,C3) | part_of(C3,C2) | part_of(C1,C2) | part_of(C2,C1) | part_of(C1,C3) | part_of(C3,C1))). (all C exists P inner_point(P,C)). (all C all P (inner_point(P,C) -> (exists C1 exists C2 (meet(P,C1,C2) & C = sum(C1,C2))))). (all C all P all Q all R (end_point(P,C) & end_point(Q,C) & end_point(R,C) -> P = Q | P = R | Q = R)). (all C all P (end_point(P,C) -> (exists Q (end_point(Q,C) & P != Q)))). (all C all C1 all C2 all P (closed(C) & meet(P,C1,C2) & C = sum(C1,C2) -> (all Q (end_point(Q,C1) -> meet(Q,C1,C2))))). (all C1 all C2 ((exists P meet(P,C1,C2)) -> (exists C C = sum(C1,C2)))). (all C all C1 ((all P (incident_c(P,C) <-> incident_c(P,C1))) -> C = C1)). (all C all P all Q all R (between_c(C,P,Q,R) <-> P != R & (exists Cpp (part_of(Cpp,C) & end_point(P,Cpp) & end_point(R,Cpp) & inner_point(Q,Cpp))))). (all O all P all Q all R (between_o(O,P,Q,R) <-> ordered_by(O,P,Q) & ordered_by(O,Q,R) | ordered_by(O,R,Q) & ordered_by(O,Q,P))). (all P all O (start_point(P,O) <-> incident_o(P,O) & (all Q (P != Q & incident_o(Q,O) -> ordered_by(O,P,Q))))). (all P all O (finish_point(P,O) <-> incident_o(P,O) & (all Q (P != Q & incident_o(Q,O) -> ordered_by(O,Q,P))))). (all O all P all Q (ordered_by(O,P,Q) -> incident_o(P,O) & incident_o(Q,O))). (all O exists C (open(C) & (all P (incident_o(P,O) <-> incident_c(P,C))))). (all P all Q all R all O (between_o(O,P,Q,R) <-> (exists C ((all P (incident_o(P,O) <-> incident_c(P,C))) & between_c(C,P,Q,R))))). (all O exists P start_point(P,O)). (all P all Q all C (open(C) & P != Q & incident_c(P,C) & incident_c(Q,C) -> (exists O ((all R (incident_o(R,O) <-> incident_c(R,C))) & ordered_by(O,P,Q))))). (all O1 all O2 ((all P all Q (ordered_by(O1,P,Q) <-> ordered_by(O2,P,Q))) -> O1 = O2)). (all C all O (C = underlying_curve(O) <-> (all P (incident_o(P,O) <-> incident_c(P,C))))). (all X all Y all P (connect(X,Y,P) <-> once(at_the_same_time(at(X,P),at(Y,P))))). (all A all B (once(at_the_same_time(A,B)) <-> once(at_the_same_time(B,A)))). (all A all B all C (once(at_the_same_time(at_the_same_time(A,B),C)) <-> once(at_the_same_time(A,at_the_same_time(B,C))))). (all A (once(A) -> once(at_the_same_time(A,A)))). (all A all B (once(at_the_same_time(A,B)) -> once(A) & once(B))). (all X all P (once(at(X,P)) <-> incident_o(P,trajectory_of(X)))). (all X exists O trajectory_of(X) = O). (all P1 all P2 all Q1 all Q2 all X all Y (once(at_the_same_time(at(X,P1),at(Y,P2))) & once(at_the_same_time(at(X,Q1),at(Y,Q2))) -> -(ordered_by(trajectory_of(X),P1,Q1) & ordered_by(trajectory_of(Y),Q2,P2)))). (all A (once(A) -> (all X exists P once(at_the_same_time(A,at(X,P)))))). -(all X all Y all P (connect(X,Y,P) <-> connect(Y,X,P))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <635,273>. Problem reduction (0.01 sec) gives 2 independent subproblems: ( <1074,218> <1074,218> ). Max nnf_size of subproblems is 1074; max cnf_max is 218. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 2 (negated): ((all C (all C1 (part_of(C1,C) | (exists P (incident_c(P,C1) & - incident_c(P,C)))))) & (all C (all C1 ((all P (- incident_c(P,C1) | incident_c(P,C))) | - part_of(C1,C)))) & (all C (all C1 ((all P (- incident_c(P,C1) | incident_c(P,C))) | (exists P (incident_c(P,C1) & - incident_c(P,C)))))) & (all C (all C1 ((exists Q (- incident_c(Q,C) & incident_c(Q,C1))) | (all C2 (=(sum(C1,C2),C) | (exists Q (incident_c(Q,C) & - incident_c(Q,C1) & - incident_c(Q,C2))) | (exists Q (- incident_c(Q,C) & incident_c(Q,C2)))))))) & (all C (all C1 ((all Q (incident_c(Q,C) | - incident_c(Q,C1))) | (all C2 (- =(sum(C1,C2),C)))))) & (all C (all C1 ((all Q (incident_c(Q,C) | - incident_c(Q,C1))) | (exists Q (- incident_c(Q,C) & incident_c(Q,C1))) | (all C2 ((exists Q (incident_c(Q,C) & - incident_c(Q,C1) & - incident_c(Q,C2))) | (exists Q (- incident_c(Q,C) & incident_c(Q,C2)))))))) & (all C (all C1 (all C2 ((all Q (incident_c(Q,C) | - incident_c(Q,C2))) | - =(sum(C1,C2),C))))) & (all C (all C1 ((exists Q (- incident_c(Q,C) & incident_c(Q,C1))) | (all C2 ((all Q (incident_c(Q,C) | - incident_c(Q,C2))) | (exists Q (incident_c(Q,C) & - incident_c(Q,C1) & - incident_c(Q,C2))) | (exists Q (- incident_c(Q,C) & incident_c(Q,C2)))))))) & (all C (all C1 (all C2 ((all Q (incident_c(Q,C1) | incident_c(Q,C2) | - incident_c(Q,C))) | - =(sum(C1,C2),C))))) & (all C (all C1 ((exists Q (- incident_c(Q,C) & incident_c(Q,C1))) | (all C2 ((all Q (incident_c(Q,C1) | incident_c(Q,C2) | - incident_c(Q,C))) | (exists Q (incident_c(Q,C) & - incident_c(Q,C1) & - incident_c(Q,C2))) | (exists Q (- incident_c(Q,C) & incident_c(Q,C2)))))))) & (all P (all C (end_point(P,C) | - incident_c(P,C) | (exists C1 (part_of(C1,C) & incident_c(P,C1) & (exists C2 (part_of(C2,C) & incident_c(P,C2) & - part_of(C1,C2) & - part_of(C2,C1)))))))) & (all P (all C (incident_c(P,C) | - end_point(P,C)))) & (all P (all C ((all C1 (- part_of(C1,C) | - incident_c(P,C1) | (all C2 (- part_of(C2,C) | - incident_c(P,C2) | part_of(C1,C2) | part_of(C2,C1))))) | - end_point(P,C)))) & (all P (all C ((all C1 (- part_of(C1,C) | - incident_c(P,C1) | (all C2 (- part_of(C2,C) | - incident_c(P,C2) | part_of(C1,C2) | part_of(C2,C1))))) | - incident_c(P,C) | (exists C1 (part_of(C1,C) & incident_c(P,C1) & (exists C2 (part_of(C2,C) & incident_c(P,C2) & - part_of(C1,C2) & - part_of(C2,C1)))))))) & (all P (all C (inner_point(P,C) | - incident_c(P,C) | end_point(P,C)))) & (all P (all C (incident_c(P,C) | - inner_point(P,C)))) & (all P (all C (- end_point(P,C) | - inner_point(P,C)))) & (all P (all C (- incident_c(P,C) | (all C1 (meet(P,C,C1) | - incident_c(P,C1) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C))) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C1)))))))) & (all P (all C (incident_c(P,C) | (all C1 (- meet(P,C,C1)))))) & (all P (all C (all C1 (incident_c(P,C1) | - meet(P,C,C1))))) & (all P (all C (all C1 ((all Q (- incident_c(Q,C) | - incident_c(Q,C1) | end_point(Q,C))) | - meet(P,C,C1))))) & (all P (all C (- incident_c(P,C) | (all C1 ((all Q (- incident_c(Q,C) | - incident_c(Q,C1) | end_point(Q,C))) | - incident_c(P,C1) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C))) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C1)))))))) & (all P (all C (all C1 ((all Q (- incident_c(Q,C) | - incident_c(Q,C1) | end_point(Q,C1))) | - meet(P,C,C1))))) & (all P (all C (- incident_c(P,C) | (all C1 ((all Q (- incident_c(Q,C) | - incident_c(Q,C1) | end_point(Q,C1))) | - incident_c(P,C1) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C))) | (exists Q (incident_c(Q,C) & incident_c(Q,C1) & - end_point(Q,C1)))))))) & (all C (closed(C) | (exists P end_point(P,C)))) & (all C ((all P - end_point(P,C)) | - closed(C))) & (all C ((all P - end_point(P,C)) | (exists P end_point(P,C)))) & (all C (open(C) | (all P - end_point(P,C)))) & (all C ((exists P end_point(P,C)) | - open(C))) & (all C ((exists P end_point(P,C)) | (all P - end_point(P,C)))) & (all C (all C1 (- part_of(C1,C) | =(C1,C) | open(C1)))) & (all C (all C1 (- part_of(C1,C) | (all C2 (- part_of(C2,C) | part_of(C1,C2) | part_of(C2,C1) | (all C3 (- part_of(C3,C) | (all P (- end_point(P,C1) | - end_point(P,C2) | - end_point(P,C3))) | part_of(C2,C3) | part_of(C3,C2) | part_of(C1,C3) | part_of(C3,C1)))))))) & (all C (exists P inner_point(P,C))) & (all C (all P (- inner_point(P,C) | (exists C1 (exists C2 (meet(P,C1,C2) & =(sum(C1,C2),C))))))) & (all C (all P (- end_point(P,C) | (all Q (- end_point(Q,C) | =(Q,P) | (all R (- end_point(R,C) | =(R,P) | =(R,Q)))))))) & (all C (all P (- end_point(P,C) | (exists Q (end_point(Q,C) & - =(Q,P)))))) & (all C (- closed(C) | (all C1 ((all C2 (- =(sum(C1,C2),C) | (all Q (- end_point(Q,C1) | meet(Q,C1,C2))) | (all P (- meet(P,C1,C2))))))))) & (all C1 (all C2 ((all P - meet(P,C1,C2)) | (exists C =(sum(C1,C2),C))))) & (all C (all C1 ((exists P (incident_c(P,C) & - incident_c(P,C1))) | (exists P (- incident_c(P,C) & incident_c(P,C1))) | =(C1,C)))) & (all C (all P (all Q (all R (between_c(C,P,Q,R) | =(R,P) | (all Cpp (- part_of(Cpp,C) | - end_point(P,Cpp) | - end_point(R,Cpp) | - inner_point(Q,Cpp)))))))) & (all C (all P (all Q (all R (- =(R,P) | - between_c(C,P,Q,R)))))) & (all C (all P (all Q (all R ((exists Cpp (part_of(Cpp,C) & end_point(P,Cpp) & end_point(R,Cpp) & inner_point(Q,Cpp))) | - between_c(C,P,Q,R)))))) & (all C (all P (all Q (all R ((exists Cpp (part_of(Cpp,C) & end_point(P,Cpp) & end_point(R,Cpp) & inner_point(Q,Cpp))) | =(R,P) | (all Cpp (- part_of(Cpp,C) | - end_point(P,Cpp) | - end_point(R,Cpp) | - inner_point(Q,Cpp)))))))) & (all O (all P (all Q (- ordered_by(O,P,Q) | (all R (between_o(O,P,Q,R) | - ordered_by(O,Q,R))))))) & (all O (all P (all Q (- ordered_by(O,Q,P) | (all R (between_o(O,P,Q,R) | - ordered_by(O,R,Q))))))) & (all O (all P (all Q (ordered_by(O,P,Q) | (all R (ordered_by(O,R,Q) | - between_o(O,P,Q,R))))))) & (all O (all P (all Q (ordered_by(O,P,Q) | ordered_by(O,Q,P) | (all R (- between_o(O,P,Q,R))))))) & (all O (all P (all Q (all R (ordered_by(O,Q,R) | ordered_by(O,R,Q) | - between_o(O,P,Q,R)))))) & (all O (all P (all Q (ordered_by(O,Q,P) | (all R (ordered_by(O,Q,R) | - between_o(O,P,Q,R))))))) & (all P (all O (start_point(P,O) | - incident_o(P,O) | (exists Q (- =(Q,P) & incident_o(Q,O) & - ordered_by(O,P,Q)))))) & (all P (all O (incident_o(P,O) | - start_point(P,O)))) & (all P (all O ((all Q (=(Q,P) | - incident_o(Q,O) | ordered_by(O,P,Q))) | - start_point(P,O)))) & (all P (all O ((all Q (=(Q,P) | - incident_o(Q,O) | ordered_by(O,P,Q))) | - incident_o(P,O) | (exists Q (- =(Q,P) & incident_o(Q,O) & - ordered_by(O,P,Q)))))) & (all P (all O (finish_point(P,O) | - incident_o(P,O) | (exists Q (- =(Q,P) & incident_o(Q,O) & - ordered_by(O,Q,P)))))) & (all P (all O (incident_o(P,O) | - finish_point(P,O)))) & (all P (all O ((all Q (=(Q,P) | - incident_o(Q,O) | ordered_by(O,Q,P))) | - finish_point(P,O)))) & (all P (all O ((all Q (=(Q,P) | - incident_o(Q,O) | ordered_by(O,Q,P))) | - incident_o(P,O) | (exists Q (- =(Q,P) & incident_o(Q,O) & - ordered_by(O,Q,P)))))) & (all O (all P (incident_o(P,O) | (all Q (- ordered_by(O,P,Q)))))) & (all O (all P (all Q (- ordered_by(O,P,Q) | incident_o(Q,O))))) & (all O (exists C (open(C) & (all P (incident_o(P,O) | - incident_c(P,C))) & (all P (incident_c(P,C) | - incident_o(P,O)))))) & (all P (all Q (all R (all O (between_o(O,P,Q,R) | (all C ((exists P (incident_o(P,O) & - incident_c(P,C))) | (exists P (- incident_o(P,O) & incident_c(P,C))) | - between_c(C,P,Q,R)))))))) & (all P (all Q (all R (all O ((exists C ((all P (incident_o(P,O) | - incident_c(P,C))) & (all P (incident_c(P,C) | - incident_o(P,O))) & between_c(C,P,Q,R))) | - between_o(O,P,Q,R)))))) & (all P (all Q (all R (all O ((exists C ((all P (incident_o(P,O) | - incident_c(P,C))) & (all P (incident_c(P,C) | - incident_o(P,O))) & between_c(C,P,Q,R))) | (all C ((exists P (incident_o(P,O) & - incident_c(P,C))) | (exists P (- incident_o(P,O) & incident_c(P,C))) | - between_c(C,P,Q,R)))))))) & (all O (exists P start_point(P,O))) & (all P (all Q (=(Q,P) | (all C (- open(C) | - incident_c(P,C) | - incident_c(Q,C) | (exists O ((all R (incident_o(R,O) | - incident_c(R,C))) & (all R (incident_c(R,C) | - incident_o(R,O))) & ordered_by(O,P,Q)))))))) & (all O1 (all O2 ((exists P (exists Q (ordered_by(O1,P,Q) & - ordered_by(O2,P,Q)))) | (exists P (exists Q (- ordered_by(O1,P,Q) & ordered_by(O2,P,Q)))) | =(O2,O1)))) & (all C (all O (=(underlying_curve(O),C) | (exists P (incident_o(P,O) & - incident_c(P,C))) | (exists P (- incident_o(P,O) & incident_c(P,C)))))) & (all C (all O ((all P (incident_o(P,O) | - incident_c(P,C))) | - =(underlying_curve(O),C)))) & (all C (all O ((all P (incident_o(P,O) | - incident_c(P,C))) | (exists P (incident_o(P,O) & - incident_c(P,C))) | (exists P (- incident_o(P,O) & incident_c(P,C)))))) & (all C (all O ((all P (incident_c(P,C) | - incident_o(P,O))) | - =(underlying_curve(O),C)))) & (all C (all O ((all P (incident_c(P,C) | - incident_o(P,O))) | (exists P (incident_o(P,O) & - incident_c(P,C))) | (exists P (- incident_o(P,O) & incident_c(P,C)))))) & (all X (all Y (all P (connect(X,Y,P) | - once(at_the_same_time(at(X,P),at(Y,P))))))) & (all X (all Y (all P (once(at_the_same_time(at(X,P),at(Y,P))) | - connect(X,Y,P))))) & (all A (all B (once(at_the_same_time(A,B)) | - once(at_the_same_time(B,A))))) & (all A (all B (once(at_the_same_time(B,A)) | - once(at_the_same_time(A,B))))) & (all A (all B (all C (once(at_the_same_time(at_the_same_time(A,B),C)) | - once(at_the_same_time(A,at_the_same_time(B,C))))))) & (all A (all B (all C (once(at_the_same_time(A,at_the_same_time(B,C))) | - once(at_the_same_time(at_the_same_time(A,B),C)))))) & (all A (- once(A) | once(at_the_same_time(A,A)))) & (all A (once(A) | (all B (- once(at_the_same_time(A,B)))))) & (all A (all B (- once(at_the_same_time(A,B)) | once(B)))) & (all X (all P (once(at(X,P)) | - incident_o(P,trajectory_of(X))))) & (all X (all P (incident_o(P,trajectory_of(X)) | - once(at(X,P))))) & (all X (exists O =(trajectory_of(X),O))) & (all P1 (all P2 (all Q1 (all Q2 (all X (- ordered_by(trajectory_of(X),P1,Q1) | (all Y (- once(at_the_same_time(at(X,P1),at(Y,P2))) | - once(at_the_same_time(at(X,Q1),at(Y,Q2))) | - ordered_by(trajectory_of(Y),Q2,P2))))))))) & (all A (- once(A) | (all X (exists P once(at_the_same_time(A,at(X,P))))))) & (exists X (exists Y (exists P (connect(X,Y,P) & - connect(Y,X,P)))))). Child search process 20921 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). part_of(A,B) | incident_c(f1(B,A),A). [assumption]. part_of(A,B) | -incident_c(f1(B,A),B). [assumption]. -incident_c(A,B) | incident_c(A,C) | -part_of(B,C). [assumption]. -incident_c(A,B) | incident_c(A,C) | incident_c(f2(C,B),B). [assumption]. -incident_c(A,B) | incident_c(A,C) | -incident_c(f2(C,B),C). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. incident_c(A,B) | -incident_c(A,C) | sum(C,D) != B. [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. incident_c(A,B) | -incident_c(A,C) | sum(D,C) != B. [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. incident_c(A,B) | incident_c(A,C) | -incident_c(A,D) | sum(B,C) != D. [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. end_point(A,B) | -incident_c(A,B) | part_of(f15(A,B),B). [assumption]. end_point(A,B) | -incident_c(A,B) | incident_c(A,f15(A,B)). [assumption]. end_point(A,B) | -incident_c(A,B) | part_of(f16(A,B),B). [assumption]. end_point(A,B) | -incident_c(A,B) | incident_c(A,f16(A,B)). [assumption]. end_point(A,B) | -incident_c(A,B) | -part_of(f15(A,B),f16(A,B)). [assumption]. end_point(A,B) | -incident_c(A,B) | -part_of(f16(A,B),f15(A,B)). [assumption]. incident_c(A,B) | -end_point(A,B). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -end_point(C,B). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f17(C,B),B). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f17(C,B)). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f18(C,B),B). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f18(C,B)). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f17(C,B),f18(C,B)). [assumption]. -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f18(C,B),f17(C,B)). [assumption]. inner_point(A,B) | -incident_c(A,B) | end_point(A,B). [assumption]. incident_c(A,B) | -inner_point(A,B). [assumption]. -end_point(A,B) | -inner_point(A,B). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),B). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),C). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | -end_point(f20(A,B,C),C). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. incident_c(A,B) | -meet(A,B,C). [assumption]. incident_c(A,B) | -meet(A,C,B). [assumption]. -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -meet(D,B,C). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | -end_point(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -meet(D,B,C). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | -end_point(f24(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. closed(A) | end_point(f25(A),A). [assumption]. -end_point(A,B) | -closed(B). [assumption]. -end_point(A,B) | end_point(f26(B),B). [assumption]. open(A) | -end_point(B,A). [assumption]. end_point(f27(A),A) | -open(A). [assumption]. end_point(f28(A),A) | -end_point(B,A). [assumption]. -part_of(A,B) | A = B | open(A). [assumption]. -part_of(A,B) | -part_of(C,B) | part_of(A,C) | part_of(C,A) | -part_of(D,B) | -end_point(E,A) | -end_point(E,C) | -end_point(E,D) | part_of(C,D) | part_of(D,C) | part_of(A,D) | part_of(D,A). [assumption]. inner_point(f29(A),A). [assumption]. -inner_point(A,B) | meet(A,f30(B,A),f31(B,A)). [assumption]. -inner_point(A,B) | sum(f30(B,A),f31(B,A)) = B. [assumption]. -end_point(A,B) | -end_point(C,B) | C = A | -end_point(D,B) | D = A | D = C. [assumption]. -end_point(A,B) | end_point(f32(B,A),B). [assumption]. -end_point(A,B) | f32(B,A) != A. [assumption]. -closed(A) | sum(B,C) != A | -end_point(D,B) | meet(D,B,C) | -meet(E,B,C). [assumption]. -meet(A,B,C) | sum(B,C) = f33(B,C). [assumption]. incident_c(f34(A,B),A) | -incident_c(f35(A,B),A) | B = A. [assumption]. incident_c(f34(A,B),A) | incident_c(f35(A,B),B) | B = A. [assumption]. -incident_c(f34(A,B),B) | -incident_c(f35(A,B),A) | B = A. [assumption]. -incident_c(f34(A,B),B) | incident_c(f35(A,B),B) | B = A. [assumption]. between_c(A,B,C,D) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. A != B | -between_c(C,B,D,A). [assumption]. part_of(f36(A,B,C,D),A) | -between_c(A,B,C,D). [assumption]. end_point(A,f36(B,A,C,D)) | -between_c(B,A,C,D). [assumption]. end_point(A,f36(B,C,D,A)) | -between_c(B,C,D,A). [assumption]. inner_point(A,f36(B,C,A,D)) | -between_c(B,C,A,D). [assumption]. part_of(f37(A,B,C,D),A) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. end_point(A,f37(B,A,C,D)) | D = A | -part_of(E,B) | -end_point(A,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. end_point(A,f37(B,C,D,A)) | A = C | -part_of(E,B) | -end_point(C,E) | -end_point(A,E) | -inner_point(D,E). [assumption]. inner_point(A,f37(B,C,A,D)) | D = C | -part_of(E,B) | -end_point(C,E) | -end_point(D,E) | -inner_point(A,E). [assumption]. -ordered_by(A,B,C) | between_o(A,B,C,D) | -ordered_by(A,C,D). [assumption]. -ordered_by(A,B,C) | between_o(A,C,B,D) | -ordered_by(A,D,B). [assumption]. ordered_by(A,B,C) | ordered_by(A,D,C) | -between_o(A,B,C,D). [assumption]. ordered_by(A,B,C) | ordered_by(A,C,B) | -between_o(A,B,C,D). [assumption]. ordered_by(A,B,C) | ordered_by(A,C,B) | -between_o(A,D,B,C). [assumption]. ordered_by(A,B,C) | ordered_by(A,B,D) | -between_o(A,C,B,D). [assumption]. start_point(A,B) | -incident_o(A,B) | f38(A,B) != A. [assumption]. start_point(A,B) | -incident_o(A,B) | incident_o(f38(A,B),B). [assumption]. start_point(A,B) | -incident_o(A,B) | -ordered_by(B,A,f38(A,B)). [assumption]. incident_o(A,B) | -start_point(A,B). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,B,A) | -start_point(B,C). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f39(B,C) != B. [assumption]. A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f39(B,C),C). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f39(B,C)). [assumption]. finish_point(A,B) | -incident_o(A,B) | f40(A,B) != A. [assumption]. finish_point(A,B) | -incident_o(A,B) | incident_o(f40(A,B),B). [assumption]. finish_point(A,B) | -incident_o(A,B) | -ordered_by(B,f40(A,B),A). [assumption]. incident_o(A,B) | -finish_point(A,B). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,A,B) | -finish_point(B,C). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f41(B,C) != B. [assumption]. A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f41(B,C),C). [assumption]. A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f41(B,C),B). [assumption]. incident_o(A,B) | -ordered_by(B,A,C). [assumption]. -ordered_by(A,B,C) | incident_o(C,A). [assumption]. open(f42(A)). [assumption]. incident_o(A,B) | -incident_c(A,f42(B)). [assumption]. incident_c(A,f42(B)) | -incident_o(A,B). [assumption]. between_o(A,B,C,D) | incident_o(f43(B,C,D,A,E),A) | -incident_o(f44(B,C,D,A,E),A) | -between_c(E,B,C,D). [assumption]. between_o(A,B,C,D) | incident_o(f43(B,C,D,A,E),A) | incident_c(f44(B,C,D,A,E),E) | -between_c(E,B,C,D). [assumption]. between_o(A,B,C,D) | -incident_c(f43(B,C,D,A,E),E) | -incident_o(f44(B,C,D,A,E),A) | -between_c(E,B,C,D). [assumption]. between_o(A,B,C,D) | -incident_c(f43(B,C,D,A,E),E) | incident_c(f44(B,C,D,A,E),E) | -between_c(E,B,C,D). [assumption]. incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -between_o(B,C,D,E). [assumption]. incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -between_o(E,B,C,D). [assumption]. between_c(f45(A,B,C,D),A,B,C) | -between_o(D,A,B,C). [assumption]. incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. start_point(f49(A),A). [assumption]. A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C). [assumption]. A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)). [assumption]. A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A). [assumption]. ordered_by(A,f51(A,B),f52(A,B)) | -ordered_by(A,f53(A,B),f54(A,B)) | B = A. [assumption]. ordered_by(A,f51(A,B),f52(A,B)) | ordered_by(B,f53(A,B),f54(A,B)) | B = A. [assumption]. -ordered_by(A,f51(B,A),f52(B,A)) | -ordered_by(B,f53(B,A),f54(B,A)) | A = B. [assumption]. -ordered_by(A,f51(B,A),f52(B,A)) | ordered_by(A,f53(B,A),f54(B,A)) | A = B. [assumption]. underlying_curve(A) = B | incident_o(f55(B,A),A) | -incident_o(f56(B,A),A). [assumption]. underlying_curve(A) = B | incident_o(f55(B,A),A) | incident_c(f56(B,A),B). [assumption]. underlying_curve(A) = B | -incident_c(f55(B,A),B) | -incident_o(f56(B,A),A). [assumption]. underlying_curve(A) = B | -incident_c(f55(B,A),B) | incident_c(f56(B,A),B). [assumption]. incident_o(A,B) | -incident_c(A,C) | underlying_curve(B) != C. [assumption]. incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | -incident_o(f58(C,B),B). [assumption]. incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | incident_c(f58(C,B),C). [assumption]. incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | -incident_o(f58(C,B),B). [assumption]. incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | incident_c(f58(C,B),C). [assumption]. incident_c(A,B) | -incident_o(A,C) | underlying_curve(C) != B. [assumption]. incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | -incident_o(f60(B,C),C). [assumption]. incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | incident_c(f60(B,C),B). [assumption]. incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | -incident_o(f60(B,C),C). [assumption]. incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | incident_c(f60(B,C),B). [assumption]. connect(A,B,C) | -once(at_the_same_time(at(A,C),at(B,C))). [assumption]. once(at_the_same_time(at(A,B),at(C,B))) | -connect(A,C,B). [assumption]. once(at_the_same_time(A,B)) | -once(at_the_same_time(B,A)). [assumption]. once(at_the_same_time(A,B)) | -once(at_the_same_time(B,A)). [assumption]. once(at_the_same_time(at_the_same_time(A,B),C)) | -once(at_the_same_time(A,at_the_same_time(B,C))). [assumption]. once(at_the_same_time(A,at_the_same_time(B,C))) | -once(at_the_same_time(at_the_same_time(A,B),C)). [assumption]. -once(A) | once(at_the_same_time(A,A)). [assumption]. once(A) | -once(at_the_same_time(A,B)). [assumption]. -once(at_the_same_time(A,B)) | once(B). [assumption]. once(at(A,B)) | -incident_o(B,trajectory_of(A)). [assumption]. incident_o(A,trajectory_of(B)) | -once(at(B,A)). [assumption]. trajectory_of(A) = f61(A). [assumption]. -ordered_by(trajectory_of(A),B,C) | -once(at_the_same_time(at(A,B),at(D,E))) | -once(at_the_same_time(at(A,C),at(D,F))) | -ordered_by(trajectory_of(D),F,E). [assumption]. -once(A) | once(at_the_same_time(A,at(B,f62(A,B)))). [assumption]. connect(c1,c2,c3). [assumption]. -connect(c2,c1,c3). [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating closed/1 1 -end_point(A,B) | -closed(B). [assumption]. 2 closed(A) | end_point(f25(A),A). [assumption]. Derived: -end_point(A,B) | end_point(f25(B),B). [resolve(1,b,2,a)]. 3 -closed(A) | sum(B,C) != A | -end_point(D,B) | meet(D,B,C) | -meet(E,B,C). [assumption]. Derived: sum(A,B) != C | -end_point(D,A) | meet(D,A,B) | -meet(E,A,B) | end_point(f25(C),C). [resolve(3,a,2,a)]. Eliminating open/1 4 end_point(f27(A),A) | -open(A). [assumption]. 5 open(A) | -end_point(B,A). [assumption]. Derived: end_point(f27(A),A) | -end_point(B,A). [resolve(4,b,5,a)]. 6 -part_of(A,B) | A = B | open(A). [assumption]. Derived: -part_of(A,B) | A = B | end_point(f27(A),A). [resolve(6,c,4,b)]. 7 open(f42(A)). [assumption]. Derived: end_point(f27(f42(A)),f42(A)). [resolve(7,a,4,b)]. 8 A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C). [assumption]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -end_point(E,C). [resolve(8,b,5,a)]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -part_of(C,E) | C = E. [resolve(8,b,6,c)]. Derived: A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_o(D,f50(B,A,f42(C))) | -incident_c(D,f42(C)). [resolve(8,b,7,a)]. 9 A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)). [assumption]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -end_point(E,C). [resolve(9,b,5,a)]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -part_of(C,E) | C = E. [resolve(9,b,6,c)]. Derived: A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_c(D,f42(C)) | -incident_o(D,f50(B,A,f42(C))). [resolve(9,b,7,a)]. 10 A = B | -open(C) | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A). [assumption]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -end_point(D,C). [resolve(10,b,5,a)]. Derived: A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -part_of(C,D) | C = D. [resolve(10,b,6,c)]. Derived: A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | ordered_by(f50(B,A,f42(C)),B,A). [resolve(10,b,7,a)]. Eliminating between_o/4 11 ordered_by(A,B,C) | ordered_by(A,D,C) | -between_o(A,B,C,D). [assumption]. 12 -ordered_by(A,B,C) | between_o(A,B,C,D) | -ordered_by(A,C,D). [assumption]. 13 -ordered_by(A,B,C) | between_o(A,C,B,D) | -ordered_by(A,D,B). [assumption]. 14 ordered_by(A,B,C) | ordered_by(A,C,B) | -between_o(A,B,C,D). [assumption]. 15 ordered_by(A,B,C) | ordered_by(A,C,B) | -between_o(A,D,B,C). [assumption]. 16 ordered_by(A,B,C) | ordered_by(A,B,D) | -between_o(A,C,B,D). [assumption]. 17 between_o(A,B,C,D) | incident_o(f43(B,C,D,A,E),A) | -incident_o(f44(B,C,D,A,E),A) | -between_c(E,B,C,D). [assumption]. Derived: incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(17,a,11,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(17,a,14,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(17,a,15,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(17,a,16,c)]. 18 between_o(A,B,C,D) | incident_o(f43(B,C,D,A,E),A) | incident_c(f44(B,C,D,A,E),E) | -between_c(E,B,C,D). [assumption]. Derived: incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(18,a,11,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(18,a,14,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(18,a,15,c)]. Derived: incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(18,a,16,c)]. 19 between_o(A,B,C,D) | -incident_c(f43(B,C,D,A,E),E) | -incident_o(f44(B,C,D,A,E),A) | -between_c(E,B,C,D). [assumption]. Derived: -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(19,a,11,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(19,a,14,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(19,a,15,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(19,a,16,c)]. 20 between_o(A,B,C,D) | -incident_c(f43(B,C,D,A,E),E) | incident_c(f44(B,C,D,A,E),E) | -between_c(E,B,C,D). [assumption]. Derived: -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(20,a,11,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(20,a,14,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(20,a,15,c)]. Derived: -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(20,a,16,c)]. 21 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -between_o(B,C,D,E). [assumption]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,C,D) | -ordered_by(B,D,E). [resolve(21,c,12,b)]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,D,C) | -ordered_by(B,E,D). [resolve(21,c,13,b)]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,17,a)]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,18,a)]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,19,a)]. Derived: incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,20,a)]. 22 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -between_o(E,B,C,D). [assumption]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,B,C) | -ordered_by(E,C,D). [resolve(22,c,12,b)]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,C,B) | -ordered_by(E,D,C). [resolve(22,c,13,b)]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,17,a)]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,18,a)]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,19,a)]. Derived: incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,20,a)]. 23 between_c(f45(A,B,C,D),A,B,C) | -between_o(D,A,B,C). [assumption]. Derived: between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,A,B) | -ordered_by(D,B,C). [resolve(23,b,12,b)]. Derived: between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,B,A) | -ordered_by(D,C,B). [resolve(23,b,13,b)]. Derived: between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,17,a)]. Derived: between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,18,a)]. Derived: between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,19,a)]. Derived: between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,20,a)]. Eliminating start_point/2 24 incident_o(A,B) | -start_point(A,B). [assumption]. 25 start_point(A,B) | -incident_o(A,B) | f38(A,B) != A. [assumption]. 26 start_point(A,B) | -incident_o(A,B) | incident_o(f38(A,B),B). [assumption]. 27 start_point(A,B) | -incident_o(A,B) | -ordered_by(B,A,f38(A,B)). [assumption]. 28 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -start_point(B,C). [assumption]. Derived: A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f38(B,C) != B. [resolve(28,d,25,a)]. Derived: A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f38(B,C),C). [resolve(28,d,26,a)]. Derived: A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f38(B,C)). [resolve(28,d,27,a)]. 29 start_point(f49(A),A). [assumption]. Derived: incident_o(f49(A),A). [resolve(29,a,24,b)]. Derived: A = f49(B) | -incident_o(A,B) | ordered_by(B,f49(B),A). [resolve(29,a,28,d)]. Eliminating finish_point/2 30 incident_o(A,B) | -finish_point(A,B). [assumption]. 31 finish_point(A,B) | -incident_o(A,B) | f40(A,B) != A. [assumption]. 32 finish_point(A,B) | -incident_o(A,B) | incident_o(f40(A,B),B). [assumption]. 33 finish_point(A,B) | -incident_o(A,B) | -ordered_by(B,f40(A,B),A). [assumption]. 34 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -finish_point(B,C). [assumption]. Derived: A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f40(B,C) != B. [resolve(34,d,31,a)]. Derived: A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f40(B,C),C). [resolve(34,d,32,a)]. Derived: A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f40(B,C),B). [resolve(34,d,33,a)]. ============================== end predicate elimination ============= Term ordering decisions: Relation symbol precedence: lex([ once, incident_c, incident_o, end_point, part_of, inner_point, ordered_by, meet, connect, between_c, =, finish_point, start_point, between_o, open, closed ]). Function symbol precedence: lex([ c1, c2, c3, at_the_same_time, sum, at, f1, f2, f3, f6, f9, f12, f15, f16, f17, f18, f30, f31, f32, f33, f34, f35, f38, f39, f40, f41, f51, f52, f53, f54, f55, f56, f57, f58, f59, f60, f62, underlying_curve, trajectory_of, f25, f26, f27, f28, f29, f42, f49, f61, f4, f5, f7, f8, f10, f11, f13, f14, f19, f20, f21, f22, f23, f24, f50, f36, f37, f45, f46, f43, f44, f47, f48 ]). After inverse_order: (no changes). Unfolding symbols: trajectory_of/1. Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 35 part_of(A,B) | incident_c(f1(B,A),A). [assumption]. 36 part_of(A,B) | -incident_c(f1(B,A),B). [assumption]. 37 -incident_c(A,B) | incident_c(A,C) | -part_of(B,C). [assumption]. 38 -incident_c(A,B) | incident_c(A,C) | incident_c(f2(C,B),B). [assumption]. 39 -incident_c(A,B) | incident_c(A,C) | -incident_c(f2(C,B),C). [assumption]. 40 -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. 41 -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. 42 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. 43 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. 44 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. 45 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. 46 incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. 47 incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. 48 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. 49 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. 50 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. 51 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. 52 incident_c(A,B) | -incident_c(A,C) | sum(C,D) != B. [assumption]. 53 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. 54 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. 55 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. 56 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. 57 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. 58 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. 59 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. 60 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. 61 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. 62 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. 63 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. 64 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. 65 incident_c(A,B) | -incident_c(A,C) | sum(D,C) != B. [assumption]. 66 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. 67 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. 68 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. 69 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. 70 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. 71 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. 72 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. 73 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. 74 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. 75 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. 76 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. 77 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. 78 incident_c(A,B) | incident_c(A,C) | -incident_c(A,D) | sum(B,C) != D. [assumption]. 79 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. 80 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. 81 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. 82 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. 83 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. 84 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. 85 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. 86 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. 87 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. 88 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. 89 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. 90 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. 91 end_point(A,B) | -incident_c(A,B) | part_of(f15(A,B),B). [assumption]. 92 end_point(A,B) | -incident_c(A,B) | incident_c(A,f15(A,B)). [assumption]. 93 end_point(A,B) | -incident_c(A,B) | part_of(f16(A,B),B). [assumption]. 94 end_point(A,B) | -incident_c(A,B) | incident_c(A,f16(A,B)). [assumption]. 95 end_point(A,B) | -incident_c(A,B) | -part_of(f15(A,B),f16(A,B)). [assumption]. 96 end_point(A,B) | -incident_c(A,B) | -part_of(f16(A,B),f15(A,B)). [assumption]. 97 incident_c(A,B) | -end_point(A,B). [assumption]. 98 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -end_point(C,B). [assumption]. 99 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f17(C,B),B). [assumption]. 100 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f17(C,B)). [assumption]. 101 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f18(C,B),B). [assumption]. 102 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f18(C,B)). [assumption]. 103 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f17(C,B),f18(C,B)). [assumption]. 104 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f18(C,B),f17(C,B)). [assumption]. 105 inner_point(A,B) | -incident_c(A,B) | end_point(A,B). [assumption]. 106 incident_c(A,B) | -inner_point(A,B). [assumption]. 107 -end_point(A,B) | -inner_point(A,B). [assumption]. 108 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. 109 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. 110 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. 111 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),B). [assumption]. 112 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),C). [assumption]. 113 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | -end_point(f20(A,B,C),C). [assumption]. 114 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. 115 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. 116 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. 117 incident_c(A,B) | -meet(A,B,C). [assumption]. 118 incident_c(A,B) | -meet(A,C,B). [assumption]. 119 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -meet(D,B,C). [assumption]. 120 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. 121 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. 122 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. 123 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),B). [assumption]. 124 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),D). [assumption]. 125 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | -end_point(f22(A,B,D),D). [assumption]. 126 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. 127 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. 128 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. 129 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -meet(D,B,C). [assumption]. 130 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. 131 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. 132 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. 133 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),B). [assumption]. 134 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),D). [assumption]. 135 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | -end_point(f24(A,B,D),D). [assumption]. 136 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. 137 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. 138 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. 139 -end_point(A,B) | end_point(f26(B),B). [assumption]. 140 end_point(f28(A),A) | -end_point(B,A). [assumption]. 141 -part_of(A,B) | -part_of(C,B) | part_of(A,C) | part_of(C,A) | -part_of(D,B) | -end_point(E,A) | -end_point(E,C) | -end_point(E,D) | part_of(C,D) | part_of(D,C) | part_of(A,D) | part_of(D,A). [assumption]. 142 inner_point(f29(A),A). [assumption]. 143 -inner_point(A,B) | meet(A,f30(B,A),f31(B,A)). [assumption]. 144 -inner_point(A,B) | sum(f30(B,A),f31(B,A)) = B. [assumption]. 145 -end_point(A,B) | -end_point(C,B) | C = A | -end_point(D,B) | D = A | D = C. [assumption]. 146 -end_point(A,B) | end_point(f32(B,A),B). [assumption]. 147 -end_point(A,B) | f32(B,A) != A. [assumption]. 149 -meet(A,B,C) | f33(B,C) = sum(B,C). [copy(148),flip(b)]. 150 incident_c(f34(A,B),A) | -incident_c(f35(A,B),A) | B = A. [assumption]. 151 incident_c(f34(A,B),A) | incident_c(f35(A,B),B) | B = A. [assumption]. 152 -incident_c(f34(A,B),B) | -incident_c(f35(A,B),A) | B = A. [assumption]. 153 -incident_c(f34(A,B),B) | incident_c(f35(A,B),B) | B = A. [assumption]. 154 between_c(A,B,C,D) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. 155 A != B | -between_c(C,B,D,A). [assumption]. 156 part_of(f36(A,B,C,D),A) | -between_c(A,B,C,D). [assumption]. 157 end_point(A,f36(B,A,C,D)) | -between_c(B,A,C,D). [assumption]. 158 end_point(A,f36(B,C,D,A)) | -between_c(B,C,D,A). [assumption]. 159 inner_point(A,f36(B,C,A,D)) | -between_c(B,C,A,D). [assumption]. 160 part_of(f37(A,B,C,D),A) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. 161 end_point(A,f37(B,A,C,D)) | D = A | -part_of(E,B) | -end_point(A,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. 162 end_point(A,f37(B,C,D,A)) | A = C | -part_of(E,B) | -end_point(C,E) | -end_point(A,E) | -inner_point(D,E). [assumption]. 163 inner_point(A,f37(B,C,A,D)) | D = C | -part_of(E,B) | -end_point(C,E) | -end_point(D,E) | -inner_point(A,E). [assumption]. 164 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f39(B,C) != B. [assumption]. 165 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f39(B,C),C). [assumption]. 166 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f39(B,C)). [assumption]. 167 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f41(B,C) != B. [assumption]. 168 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f41(B,C),C). [assumption]. 169 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f41(B,C),B). [assumption]. 170 incident_o(A,B) | -ordered_by(B,A,C). [assumption]. 171 -ordered_by(A,B,C) | incident_o(C,A). [assumption]. 172 incident_o(A,B) | -incident_c(A,f42(B)). [assumption]. 173 incident_c(A,f42(B)) | -incident_o(A,B). [assumption]. 174 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. 175 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. 176 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. 177 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. 178 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. 179 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. 180 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. 181 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. 182 between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. 183 between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. 184 between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. 185 between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. 186 ordered_by(A,f51(A,B),f52(A,B)) | -ordered_by(A,f53(A,B),f54(A,B)) | B = A. [assumption]. 187 ordered_by(A,f51(A,B),f52(A,B)) | ordered_by(B,f53(A,B),f54(A,B)) | B = A. [assumption]. 188 -ordered_by(A,f51(B,A),f52(B,A)) | -ordered_by(B,f53(B,A),f54(B,A)) | A = B. [assumption]. 189 -ordered_by(A,f51(B,A),f52(B,A)) | ordered_by(A,f53(B,A),f54(B,A)) | A = B. [assumption]. 190 underlying_curve(A) = B | incident_o(f55(B,A),A) | -incident_o(f56(B,A),A). [assumption]. 191 underlying_curve(A) = B | incident_o(f55(B,A),A) | incident_c(f56(B,A),B). [assumption]. 192 underlying_curve(A) = B | -incident_c(f55(B,A),B) | -incident_o(f56(B,A),A). [assumption]. 193 underlying_curve(A) = B | -incident_c(f55(B,A),B) | incident_c(f56(B,A),B). [assumption]. 194 incident_o(A,B) | -incident_c(A,C) | underlying_curve(B) != C. [assumption]. 195 incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | -incident_o(f58(C,B),B). [assumption]. 196 incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | incident_c(f58(C,B),C). [assumption]. 197 incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | -incident_o(f58(C,B),B). [assumption]. 198 incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | incident_c(f58(C,B),C). [assumption]. 199 incident_c(A,B) | -incident_o(A,C) | underlying_curve(C) != B. [assumption]. 200 incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | -incident_o(f60(B,C),C). [assumption]. 201 incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | incident_c(f60(B,C),B). [assumption]. 202 incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | -incident_o(f60(B,C),C). [assumption]. 203 incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | incident_c(f60(B,C),B). [assumption]. 204 connect(A,B,C) | -once(at_the_same_time(at(A,C),at(B,C))). [assumption]. 205 once(at_the_same_time(at(A,B),at(C,B))) | -connect(A,C,B). [assumption]. 206 once(at_the_same_time(A,B)) | -once(at_the_same_time(B,A)). [assumption]. 207 once(at_the_same_time(at_the_same_time(A,B),C)) | -once(at_the_same_time(A,at_the_same_time(B,C))). [assumption]. 208 once(at_the_same_time(A,at_the_same_time(B,C))) | -once(at_the_same_time(at_the_same_time(A,B),C)). [assumption]. 209 -once(A) | once(at_the_same_time(A,A)). [assumption]. 210 once(A) | -once(at_the_same_time(A,B)). [assumption]. 211 -once(at_the_same_time(A,B)) | once(B). [assumption]. 214 trajectory_of(A) = f61(A). [assumption]. 216 -ordered_by(f61(A),B,C) | -once(at_the_same_time(at(A,B),at(D,E))) | -once(at_the_same_time(at(A,C),at(D,F))) | -ordered_by(f61(D),F,E). [copy(215),rewrite(214(1),214(11))]. 217 -once(A) | once(at_the_same_time(A,at(B,f62(A,B)))). [assumption]. 218 connect(c1,c2,c3). [assumption]. 219 -connect(c2,c1,c3). [assumption]. 220 -end_point(A,B) | end_point(f25(B),B). [resolve(1,b,2,a)]. 221 sum(A,B) != C | -end_point(D,A) | meet(D,A,B) | -meet(E,A,B) | end_point(f25(C),C). [resolve(3,a,2,a)]. 222 end_point(f27(A),A) | -end_point(B,A). [resolve(4,b,5,a)]. 223 -part_of(A,B) | A = B | end_point(f27(A),A). [resolve(6,c,4,b)]. 224 end_point(f27(f42(A)),f42(A)). [resolve(7,a,4,b)]. 225 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -end_point(E,C). [resolve(8,b,5,a)]. 226 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -part_of(C,E) | C = E. [resolve(8,b,6,c)]. 227 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_o(D,f50(B,A,f42(C))) | -incident_c(D,f42(C)). [resolve(8,b,7,a)]. 228 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -end_point(E,C). [resolve(9,b,5,a)]. 229 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -part_of(C,E) | C = E. [resolve(9,b,6,c)]. 230 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_c(D,f42(C)) | -incident_o(D,f50(B,A,f42(C))). [resolve(9,b,7,a)]. 231 A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -end_point(D,C). [resolve(10,b,5,a)]. 232 A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -part_of(C,D) | C = D. [resolve(10,b,6,c)]. 233 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | ordered_by(f50(B,A,f42(C)),B,A). [resolve(10,b,7,a)]. 234 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(17,a,11,c)]. 235 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(17,a,14,c)]. 236 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(17,a,15,c)]. 237 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(17,a,16,c)]. 238 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(18,a,11,c)]. 239 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(18,a,14,c)]. 240 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(18,a,15,c)]. 241 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(18,a,16,c)]. 242 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(19,a,11,c)]. 243 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(19,a,14,c)]. 244 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(19,a,15,c)]. 245 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(19,a,16,c)]. 246 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(20,a,11,c)]. 247 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(20,a,14,c)]. 248 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(20,a,15,c)]. 249 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(20,a,16,c)]. 250 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,C,D) | -ordered_by(B,D,E). [resolve(21,c,12,b)]. 251 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,D,C) | -ordered_by(B,E,D). [resolve(21,c,13,b)]. 252 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,17,a)]. 253 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,18,a)]. 254 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,19,a)]. 255 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,20,a)]. 256 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,B,C) | -ordered_by(E,C,D). [resolve(22,c,12,b)]. 257 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,C,B) | -ordered_by(E,D,C). [resolve(22,c,13,b)]. 258 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,17,a)]. 259 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,18,a)]. 260 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,19,a)]. 261 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,20,a)]. 262 between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,A,B) | -ordered_by(D,B,C). [resolve(23,b,12,b)]. 263 between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,B,A) | -ordered_by(D,C,B). [resolve(23,b,13,b)]. 264 between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,17,a)]. 265 between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,18,a)]. 266 between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,19,a)]. 267 between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,20,a)]. 268 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f38(B,C) != B. [resolve(28,d,25,a)]. 269 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f38(B,C),C). [resolve(28,d,26,a)]. 270 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f38(B,C)). [resolve(28,d,27,a)]. 271 incident_o(f49(A),A). [resolve(29,a,24,b)]. 273 f49(A) = B | -incident_o(B,A) | ordered_by(A,f49(A),B). [copy(272),flip(a)]. 274 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f40(B,C) != B. [resolve(34,d,31,a)]. 275 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f40(B,C),C). [resolve(34,d,32,a)]. 276 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f40(B,C),B). [resolve(34,d,33,a)]. 277 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | -incident_c(f6(A,B),A) | -incident_c(f8(A,B,C),A). [factor(53,a,d)]. 278 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | -incident_c(f6(A,B),A) | incident_c(f8(A,B,C),C). [factor(54,a,d)]. 279 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | incident_c(f7(A,B,A),A). [factor(54,a,e)]. 280 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | -incident_c(f7(A,B,A),B). [factor(56,a,e)]. 281 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | -incident_c(f7(A,B,A),A). [factor(58,a,e)]. 282 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | incident_c(f6(A,B),B) | -incident_c(f8(A,B,C),A). [factor(59,a,d)]. 283 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | incident_c(f6(A,B),B) | incident_c(f8(A,B,C),C). [factor(60,a,d)]. 284 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | incident_c(f6(A,B),B) | incident_c(f7(A,B,A),A). [factor(60,a,e)]. 285 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | incident_c(f6(A,B),B) | -incident_c(f7(A,B,A),B). [factor(62,a,e)]. 286 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | incident_c(f6(A,B),B) | -incident_c(f7(A,B,A),A). [factor(64,a,e)]. 287 -incident_c(f9(A,B),A) | incident_c(f10(A,B,C),A) | -incident_c(f10(A,B,C),C) | -incident_c(f11(A,B,C),A). [factor(66,b,d)]. 288 -incident_c(f9(A,B),A) | incident_c(f10(A,B,C),A) | -incident_c(f10(A,B,C),C) | incident_c(f11(A,B,C),C). [factor(67,b,d)]. 289 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | incident_c(f10(A,A,B),A) | -incident_c(f11(A,A,B),A). [factor(72,a,b)]. 290 incident_c(f9(A,B),B) | incident_c(f10(A,B,C),A) | -incident_c(f10(A,B,C),C) | -incident_c(f11(A,B,C),A). [factor(72,b,d)]. 291 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | incident_c(f10(A,A,B),A) | incident_c(f11(A,A,B),B). [factor(73,a,b)]. 292 incident_c(f9(A,B),B) | incident_c(f10(A,B,C),A) | -incident_c(f10(A,B,C),C) | incident_c(f11(A,B,C),C). [factor(73,b,d)]. 293 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | -incident_c(f10(A,A,B),A) | -incident_c(f11(A,A,B),A). [factor(74,a,b)]. 294 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | -incident_c(f10(A,A,B),A) | incident_c(f11(A,A,B),B). [factor(75,a,b)]. 295 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | -incident_c(f10(A,A,B),B) | -incident_c(f11(A,A,B),A). [factor(76,a,b)]. 296 incident_c(f9(A,A),A) | -incident_c(f9(A,A),B) | -incident_c(f10(A,A,B),B) | incident_c(f11(A,A,B),B). [factor(77,a,b)]. 297 incident_c(A,B) | -incident_c(A,C) | sum(B,B) != C. [factor(78,a,b)]. 298 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | incident_c(f13(A,B,C),A) | -incident_c(f14(A,B,C),A). [factor(79,a,d)]. 299 -incident_c(f12(A,B),A) | incident_c(C,B) | -incident_c(C,A) | incident_c(f13(A,B,B),A) | -incident_c(f14(A,B,B),A). [factor(79,b,c)]. 300 -incident_c(f12(A,B),A) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | incident_c(f13(A,B,C),A). [factor(79,d,f)]. 301 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | incident_c(f13(A,B,C),A) | incident_c(f14(A,B,C),C). [factor(80,a,d)]. 302 -incident_c(f12(A,B),A) | incident_c(C,B) | -incident_c(C,A) | incident_c(f13(A,B,B),A) | incident_c(f14(A,B,B),B). [factor(80,b,c)]. 303 -incident_c(f12(A,B),A) | incident_c(f14(A,B,B),B) | -incident_c(f14(A,B,B),A) | incident_c(f13(A,B,B),A). [factor(80,b,f),merge(c)]. 304 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | -incident_c(f13(A,B,C),B) | -incident_c(f14(A,B,C),A). [factor(81,a,d)]. 305 -incident_c(f12(A,B),A) | incident_c(C,B) | -incident_c(C,A) | -incident_c(f13(A,B,B),B) | -incident_c(f14(A,B,B),A). [factor(81,b,c)]. 306 -incident_c(f12(A,B),A) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | -incident_c(f13(A,B,C),B). [factor(81,d,f)]. 307 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | -incident_c(f13(A,B,C),B) | incident_c(f14(A,B,C),C). [factor(82,a,d)]. 308 -incident_c(f12(A,B),A) | incident_c(C,B) | -incident_c(C,A) | -incident_c(f13(A,B,B),B) | incident_c(f14(A,B,B),B). [factor(82,b,c)]. 309 -incident_c(f12(A,B),A) | incident_c(f14(A,B,B),B) | -incident_c(f14(A,B,B),A) | -incident_c(f13(A,B,B),B). [factor(82,b,f),merge(c)]. 310 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | -incident_c(f13(A,B,C),C) | -incident_c(f14(A,B,C),A). [factor(83,a,d)]. 311 -incident_c(f12(A,B),A) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | -incident_c(f13(A,B,C),C). [factor(83,d,f)]. 312 -incident_c(f12(A,B),A) | incident_c(f12(A,B),B) | incident_c(f12(A,B),C) | -incident_c(f13(A,B,C),C) | incident_c(f14(A,B,C),C). [factor(84,a,d)]. 313 incident_c(f12(A,B),B) | -incident_c(f12(A,B),A) | incident_c(f13(A,B,B),A) | -incident_c(f14(A,B,B),A). [factor(85,a,c),merge(b)]. 314 incident_c(f12(A,B),B) | incident_c(C,B) | -incident_c(C,A) | incident_c(f13(A,B,B),A) | -incident_c(f14(A,B,B),A). [factor(85,b,c)]. 315 incident_c(f12(A,B),B) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | incident_c(f13(A,B,C),A). [factor(85,d,f)]. 316 incident_c(f12(A,B),B) | -incident_c(f12(A,B),A) | incident_c(f13(A,B,B),A) | incident_c(f14(A,B,B),B). [factor(86,a,c),merge(b)]. 317 incident_c(f12(A,B),B) | incident_c(C,B) | -incident_c(C,A) | incident_c(f13(A,B,B),A) | incident_c(f14(A,B,B),B). [factor(86,b,c)]. 318 incident_c(f12(A,B),B) | incident_c(f14(A,B,B),B) | -incident_c(f14(A,B,B),A) | incident_c(f13(A,B,B),A). [factor(86,b,f),merge(c)]. 319 incident_c(f12(A,B),B) | -incident_c(f12(A,B),A) | -incident_c(f13(A,B,B),B) | -incident_c(f14(A,B,B),A). [factor(87,a,c),merge(b)]. 320 incident_c(f12(A,B),B) | incident_c(C,B) | -incident_c(C,A) | -incident_c(f13(A,B,B),B) | -incident_c(f14(A,B,B),A). [factor(87,b,c)]. 321 incident_c(f12(A,B),B) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | -incident_c(f13(A,B,C),B). [factor(87,d,f)]. 322 incident_c(f12(A,B),B) | -incident_c(f12(A,B),A) | -incident_c(f13(A,B,B),B) | incident_c(f14(A,B,B),B). [factor(88,a,c),merge(b)]. 323 incident_c(f12(A,B),B) | incident_c(C,B) | -incident_c(C,A) | -incident_c(f13(A,B,B),B) | incident_c(f14(A,B,B),B). [factor(88,b,c)]. 324 incident_c(f12(A,B),B) | incident_c(f14(A,B,B),B) | -incident_c(f14(A,B,B),A) | -incident_c(f13(A,B,B),B). [factor(88,b,f),merge(c)]. 325 incident_c(f12(A,B),B) | incident_c(f14(A,B,C),B) | incident_c(f14(A,B,C),C) | -incident_c(f14(A,B,C),A) | -incident_c(f13(A,B,C),C). [factor(89,d,f)]. 326 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -end_point(C,B). [factor(98,a,c),merge(c),merge(e)]. 327 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | part_of(f17(C,B),B). [factor(99,a,c),merge(c),merge(e)]. 328 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | incident_c(C,f17(C,B)). [factor(100,a,c),merge(c),merge(e)]. 329 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | part_of(f18(C,B),B). [factor(101,a,c),merge(c),merge(e)]. 330 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | incident_c(C,f18(C,B)). [factor(102,a,c),merge(c),merge(e)]. 331 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | -part_of(f17(C,B),f18(C,B)). [factor(103,a,c),merge(c),merge(e)]. 332 -part_of(A,B) | -incident_c(C,A) | part_of(A,A) | -incident_c(C,B) | -part_of(f18(C,B),f17(C,B)). [factor(104,a,c),merge(c),merge(e)]. 333 -incident_c(A,B) | meet(A,B,B) | incident_c(f19(A,B,B),B) | incident_c(f20(A,B,B),B). [factor(108,a,c)]. 334 -incident_c(A,B) | meet(A,B,B) | incident_c(f19(A,B,B),B) | -end_point(f20(A,B,B),B). [factor(110,a,c)]. 335 -incident_c(A,B) | meet(A,B,B) | -end_point(f19(A,B,B),B) | incident_c(f20(A,B,B),B). [factor(114,a,c)]. 336 -incident_c(A,B) | meet(A,B,B) | -end_point(f19(A,B,B),B) | -end_point(f20(A,B,B),B). [factor(116,a,c)]. 337 -incident_c(A,B) | end_point(A,B) | -meet(C,B,B). [factor(119,a,b)]. 338 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),B) | incident_c(f22(A,B,C),B). [factor(120,a,b),merge(d)]. 339 -incident_c(A,B) | end_point(A,B) | incident_c(f21(A,B,B),B) | incident_c(f22(A,B,B),B). [factor(120,a,c),merge(b),merge(d)]. 340 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | incident_c(f21(A,B,B),B) | incident_c(f22(A,B,B),B). [factor(120,a,e),merge(c)]. 341 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),B) | incident_c(f22(A,B,C),C). [factor(121,a,b),merge(d)]. 342 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),B) | -end_point(f22(A,B,C),C). [factor(122,a,b),merge(d)]. 343 -incident_c(A,B) | end_point(A,B) | incident_c(f21(A,B,B),B) | -end_point(f22(A,B,B),B). [factor(122,a,c),merge(b),merge(d)]. 344 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | incident_c(f21(A,B,B),B) | -end_point(f22(A,B,B),B). [factor(122,a,e),merge(c)]. 345 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),C) | incident_c(f22(A,B,C),B). [factor(123,a,b),merge(d)]. 346 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),C) | incident_c(f22(A,B,C),C). [factor(124,a,b),merge(d)]. 347 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | incident_c(f21(A,B,C),C) | -end_point(f22(A,B,C),C). [factor(125,a,b),merge(d)]. 348 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -end_point(f21(A,B,C),B) | incident_c(f22(A,B,C),B). [factor(126,a,b),merge(d)]. 349 -incident_c(A,B) | end_point(A,B) | -end_point(f21(A,B,B),B) | incident_c(f22(A,B,B),B). [factor(126,a,c),merge(b),merge(d)]. 350 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | -end_point(f21(A,B,B),B) | incident_c(f22(A,B,B),B). [factor(126,a,e),merge(c)]. 351 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -end_point(f21(A,B,C),B) | incident_c(f22(A,B,C),C). [factor(127,a,b),merge(d)]. 352 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -end_point(f21(A,B,C),B) | -end_point(f22(A,B,C),C). [factor(128,a,b),merge(d)]. 353 -incident_c(A,B) | end_point(A,B) | -end_point(f21(A,B,B),B) | -end_point(f22(A,B,B),B). [factor(128,a,c),merge(b),merge(d)]. 354 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | -end_point(f21(A,B,B),B) | -end_point(f22(A,B,B),B). [factor(128,a,e),merge(c)]. 355 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),B) | incident_c(f24(A,B,C),B). [factor(130,a,b),merge(d)]. 356 -incident_c(A,B) | end_point(A,B) | incident_c(f23(A,B,B),B) | incident_c(f24(A,B,B),B). [factor(130,a,c),merge(b),merge(d)]. 357 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | incident_c(f23(A,B,B),B) | incident_c(f24(A,B,B),B). [factor(130,a,e),merge(c)]. 358 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),B) | incident_c(f24(A,B,C),C). [factor(131,a,b),merge(d)]. 359 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),B) | -end_point(f24(A,B,C),C). [factor(132,a,b),merge(d)]. 360 -incident_c(A,B) | end_point(A,B) | incident_c(f23(A,B,B),B) | -end_point(f24(A,B,B),B). [factor(132,a,c),merge(b),merge(d)]. 361 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | incident_c(f23(A,B,B),B) | -end_point(f24(A,B,B),B). [factor(132,a,e),merge(c)]. 362 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),C) | incident_c(f24(A,B,C),B). [factor(133,a,b),merge(d)]. 363 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),C) | incident_c(f24(A,B,C),C). [factor(134,a,b),merge(d)]. 364 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | incident_c(f23(A,B,C),C) | -end_point(f24(A,B,C),C). [factor(135,a,b),merge(d)]. 365 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -end_point(f23(A,B,C),B) | incident_c(f24(A,B,C),B). [factor(136,a,b),merge(d)]. 366 -incident_c(A,B) | end_point(A,B) | -end_point(f23(A,B,B),B) | incident_c(f24(A,B,B),B). [factor(136,a,c),merge(b),merge(d)]. 367 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | -end_point(f23(A,B,B),B) | incident_c(f24(A,B,B),B). [factor(136,a,e),merge(c)]. 368 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -end_point(f23(A,B,C),B) | incident_c(f24(A,B,C),C). [factor(137,a,b),merge(d)]. 369 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -end_point(f23(A,B,C),B) | -end_point(f24(A,B,C),C). [factor(138,a,b),merge(d)]. 370 -incident_c(A,B) | end_point(A,B) | -end_point(f23(A,B,B),B) | -end_point(f24(A,B,B),B). [factor(138,a,c),merge(b),merge(d)]. 371 -incident_c(A,B) | -incident_c(C,B) | end_point(C,B) | -end_point(f23(A,B,B),B) | -end_point(f24(A,B,B),B). [factor(138,a,e),merge(c)]. 373 -part_of(A,B) | part_of(A,A) | -end_point(C,A). [factor(141,c,i),merge(b),merge(d),merge(e),merge(g),merge(h),merge(i),merge(j),merge(k)]. 374 incident_o(f47(A,B,C,D,E),D) | -incident_c(f47(A,B,C,D,E),f46(A,B,C,D)) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [factor(174,a,c)]. 375 incident_o(f47(A,B,C,D,E),D) | -incident_c(f47(A,B,C,D,E),f46(A,B,C,D)) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [factor(175,a,c)]. 376 incident_c(f48(A,B,C,D,E),f46(A,B,C,D)) | -incident_o(f48(A,B,C,D,E),D) | incident_o(f47(A,B,C,D,E),D) | -between_c(E,A,B,C). [factor(178,b,d)]. 377 incident_c(f48(A,B,C,D,E),f46(A,B,C,D)) | -incident_o(f48(A,B,C,D,E),D) | -incident_c(f47(A,B,C,D,E),E) | -between_c(E,A,B,C). [factor(180,b,d)]. 378 incident_o(f57(A,B),B) | -incident_c(f57(A,B),A) | -incident_o(f58(A,B),B). [factor(195,a,c)]. 379 incident_o(f57(A,B),B) | -incident_c(f57(A,B),A) | incident_c(f58(A,B),A). [factor(196,a,c)]. 380 incident_c(f60(A,B),A) | -incident_o(f60(A,B),B) | incident_o(f59(A,B),B). [factor(200,b,d)]. 381 incident_c(f60(A,B),A) | -incident_o(f60(A,B),B) | -incident_c(f59(A,B),A). [factor(202,b,d)]. 382 incident_o(A,f61(B)) | -once(at(B,A)). [back_rewrite(213),rewrite(214(1))]. 383 once(at(A,B)) | -incident_o(B,f61(A)). [back_rewrite(212),rewrite(214(3))]. 384 -ordered_by(f61(A),B,C) | -once(at_the_same_time(at(A,B),at(A,C))) | -once(at_the_same_time(at(A,C),at(A,B))). [factor(216,a,d)]. 385 -ordered_by(f61(A),B,B) | -once(at_the_same_time(at(A,B),at(C,D))) | -ordered_by(f61(C),D,D). [factor(216,b,c)]. 386 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(B,f50(B,A,C)) | -end_point(D,C). [factor(225,b,e)]. 387 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(A,f50(B,A,C)) | -end_point(D,C). [factor(225,c,e)]. 388 A = B | -incident_c(B,A) | -incident_c(A,A) | incident_o(C,f50(B,A,A)) | -incident_c(C,A) | -part_of(A,B). [factor(226,a,g)]. 389 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(B,f50(B,A,C)) | -part_of(C,D) | C = D. [factor(226,b,e)]. 390 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(A,f50(B,A,C)) | -part_of(C,D) | C = D. [factor(226,c,e)]. 391 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_o(B,f50(B,A,f42(C))). [factor(227,b,e)]. 392 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_o(A,f50(B,A,f42(C))). [factor(227,c,e)]. 393 A = B | -incident_c(B,A) | -incident_c(A,A) | incident_c(C,A) | -incident_o(C,f50(B,A,A)) | -part_of(A,B). [factor(229,a,g)]. 394 A = B | -incident_c(B,A) | -incident_c(A,A) | ordered_by(f50(B,A,A),B,A) | -part_of(A,B). [factor(232,a,f)]. 395 incident_o(f43(A,B,A,C,D),C) | -incident_o(f44(A,B,A,C,D),C) | -between_c(D,A,B,A) | ordered_by(C,A,B). [factor(234,d,e)]. 396 incident_o(f43(A,A,B,C,D),C) | -incident_o(f44(A,A,B,C,D),C) | -between_c(D,A,A,B) | ordered_by(C,A,A). [factor(235,d,e)]. 397 incident_o(f43(A,B,B,C,D),C) | -incident_o(f44(A,B,B,C,D),C) | -between_c(D,A,B,B) | ordered_by(C,B,B). [factor(236,d,e)]. 398 incident_o(f43(A,B,A,C,D),C) | -incident_o(f44(A,B,A,C,D),C) | -between_c(D,A,B,A) | ordered_by(C,B,A). [factor(237,d,e)]. 399 incident_o(f43(A,B,A,C,D),C) | incident_c(f44(A,B,A,C,D),D) | -between_c(D,A,B,A) | ordered_by(C,A,B). [factor(238,d,e)]. 400 incident_o(f43(A,A,B,C,D),C) | incident_c(f44(A,A,B,C,D),D) | -between_c(D,A,A,B) | ordered_by(C,A,A). [factor(239,d,e)]. 401 incident_o(f43(A,B,B,C,D),C) | incident_c(f44(A,B,B,C,D),D) | -between_c(D,A,B,B) | ordered_by(C,B,B). [factor(240,d,e)]. 402 incident_o(f43(A,B,A,C,D),C) | incident_c(f44(A,B,A,C,D),D) | -between_c(D,A,B,A) | ordered_by(C,B,A). [factor(241,d,e)]. 403 -incident_c(f43(A,B,A,C,D),D) | -incident_o(f44(A,B,A,C,D),C) | -between_c(D,A,B,A) | ordered_by(C,A,B). [factor(242,d,e)]. 404 -incident_c(f43(A,A,B,C,D),D) | -incident_o(f44(A,A,B,C,D),C) | -between_c(D,A,A,B) | ordered_by(C,A,A). [factor(243,d,e)]. 405 -incident_c(f43(A,B,B,C,D),D) | -incident_o(f44(A,B,B,C,D),C) | -between_c(D,A,B,B) | ordered_by(C,B,B). [factor(244,d,e)]. 406 -incident_c(f43(A,B,A,C,D),D) | -incident_o(f44(A,B,A,C,D),C) | -between_c(D,A,B,A) | ordered_by(C,B,A). [factor(245,d,e)]. 407 -incident_c(f43(A,B,A,C,D),D) | incident_c(f44(A,B,A,C,D),D) | -between_c(D,A,B,A) | ordered_by(C,A,B). [factor(246,d,e)]. 408 -incident_c(f43(A,A,B,C,D),D) | incident_c(f44(A,A,B,C,D),D) | -between_c(D,A,A,B) | ordered_by(C,A,A). [factor(247,d,e)]. 409 -incident_c(f43(A,B,B,C,D),D) | incident_c(f44(A,B,B,C,D),D) | -between_c(D,A,B,B) | ordered_by(C,B,B). [factor(248,d,e)]. 410 -incident_c(f43(A,B,A,C,D),D) | incident_c(f44(A,B,A,C,D),D) | -between_c(D,A,B,A) | ordered_by(C,B,A). [factor(249,d,e)]. 411 incident_o(A,B) | -incident_c(A,f45(C,C,C,B)) | -ordered_by(B,C,C). [factor(250,c,d)]. 412 incident_o(f43(A,B,C,D,E),D) | -incident_c(f43(A,B,C,D,E),f45(A,B,C,D)) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [factor(252,a,c)]. 413 incident_o(f43(A,B,C,D,E),D) | -incident_c(f43(A,B,C,D,E),f45(A,B,C,D)) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [factor(253,a,c)]. 414 incident_c(A,f45(B,B,B,C)) | -incident_o(A,C) | -ordered_by(C,B,B). [factor(256,c,d)]. 415 incident_c(f44(A,B,C,D,E),f45(A,B,C,D)) | -incident_o(f44(A,B,C,D,E),D) | incident_o(f43(A,B,C,D,E),D) | -between_c(E,A,B,C). [factor(258,b,d)]. 416 incident_c(f44(A,B,C,D,E),f45(A,B,C,D)) | -incident_o(f44(A,B,C,D,E),D) | -incident_c(f43(A,B,C,D,E),E) | -between_c(E,A,B,C). [factor(260,b,d)]. 417 between_c(f45(A,A,A,B),A,A,A) | -ordered_by(B,A,A). [factor(262,b,c)]. 418 -ordered_by(f61(A),B,B) | -once(at_the_same_time(at(A,B),at(A,B))). [factor(384,b,c)]. 419 A = B | -incident_c(B,A) | -incident_c(A,A) | incident_o(B,f50(B,A,A)) | -part_of(A,B). [factor(388,b,e)]. 420 A = B | -incident_c(B,A) | -incident_c(A,A) | incident_o(A,f50(B,A,A)) | -part_of(A,B). [factor(388,c,e)]. end_of_list. formulas(demodulators). 214 trajectory_of(A) = f61(A). [assumption]. end_of_list. ============================== end of clauses for search ============= ============================== SEARCH ================================ % Starting search at 0.07 seconds. given #1 (I,wt=8): 35 part_of(A,B) | incident_c(f1(B,A),A). [assumption]. given #2 (I,wt=8): 36 part_of(A,B) | -incident_c(f1(B,A),B). [assumption]. given #3 (I,wt=9): 37 -incident_c(A,B) | incident_c(A,C) | -part_of(B,C). [assumption]. given #4 (I,wt=11): 38 -incident_c(A,B) | incident_c(A,C) | incident_c(f2(C,B),B). [assumption]. given #5 (I,wt=11): 39 -incident_c(A,B) | incident_c(A,C) | -incident_c(f2(C,B),C). [assumption]. given #6 (I,wt=22): 40 -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. given #7 (I,wt=22): 41 -incident_c(f3(A,B),A) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. given #8 (I,wt=22): 42 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. given #9 (I,wt=22): 43 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. given #10 (I,wt=22): 44 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. given #11 (I,wt=22): 45 -incident_c(f3(A,B),A) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. given #12 (I,wt=22): 46 incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | -incident_c(f5(A,B,C),A). [assumption]. given #13 (I,wt=22): 47 incident_c(f3(A,B),B) | sum(B,C) = A | incident_c(f4(A,B,C),A) | incident_c(f5(A,B,C),C). [assumption]. given #14 (I,wt=22): 48 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | -incident_c(f5(A,B,C),A). [assumption]. given #15 (I,wt=22): 49 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),B) | incident_c(f5(A,B,C),C). [assumption]. given #16 (I,wt=22): 50 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | -incident_c(f5(A,B,C),A). [assumption]. given #17 (I,wt=22): 51 incident_c(f3(A,B),B) | sum(B,C) = A | -incident_c(f4(A,B,C),C) | incident_c(f5(A,B,C),C). [assumption]. given #18 (I,wt=11): 52 incident_c(A,B) | -incident_c(A,C) | sum(C,D) != B. [assumption]. given #19 (I,wt=23): 53 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. given #20 (I,wt=23): 54 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. given #21 (I,wt=23): 55 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. given #22 (I,wt=23): 56 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. given #23 (I,wt=23): 57 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. given #24 (I,wt=23): 58 incident_c(A,B) | -incident_c(A,C) | -incident_c(f6(B,C),B) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. given #25 (I,wt=23): 59 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | -incident_c(f8(B,C,D),B). [assumption]. given #26 (I,wt=23): 60 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | incident_c(f7(B,C,D),B) | incident_c(f8(B,C,D),D). [assumption]. given #27 (I,wt=23): 61 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | -incident_c(f8(B,C,D),B). [assumption]. given #28 (I,wt=23): 62 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),C) | incident_c(f8(B,C,D),D). [assumption]. given #29 (I,wt=23): 63 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | -incident_c(f8(B,C,D),B). [assumption]. given #30 (I,wt=23): 64 incident_c(A,B) | -incident_c(A,C) | incident_c(f6(B,C),C) | -incident_c(f7(B,C,D),D) | incident_c(f8(B,C,D),D). [assumption]. given #31 (I,wt=11): 65 incident_c(A,B) | -incident_c(A,C) | sum(D,C) != B. [assumption]. given #32 (I,wt=23): 66 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. given #33 (I,wt=23): 67 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. given #34 (I,wt=23): 68 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. given #35 (I,wt=23): 69 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. given #36 (I,wt=23): 70 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. given #37 (I,wt=23): 71 -incident_c(f9(A,B),A) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. given #38 (I,wt=23): 72 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | -incident_c(f11(A,B,D),A). [assumption]. given #39 (I,wt=23): 73 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | incident_c(f10(A,B,D),A) | incident_c(f11(A,B,D),D). [assumption]. given #40 (I,wt=23): 74 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | -incident_c(f11(A,B,D),A). [assumption]. given #41 (I,wt=23): 75 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),B) | incident_c(f11(A,B,D),D). [assumption]. given #42 (I,wt=23): 76 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | -incident_c(f11(A,B,D),A). [assumption]. given #43 (I,wt=23): 77 incident_c(f9(A,B),B) | incident_c(C,A) | -incident_c(C,D) | -incident_c(f10(A,B,D),D) | incident_c(f11(A,B,D),D). [assumption]. given #44 (I,wt=14): 78 incident_c(A,B) | incident_c(A,C) | -incident_c(A,D) | sum(B,C) != D. [assumption]. given #45 (I,wt=26): 79 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. given #46 (I,wt=26): 80 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. given #47 (I,wt=26): 81 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. given #48 (I,wt=26): 82 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. given #49 (I,wt=26): 83 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. given #50 (I,wt=26): 84 -incident_c(f12(A,B),A) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. given #51 (I,wt=26): 85 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | -incident_c(f14(A,B,D),A). [assumption]. given #52 (I,wt=26): 86 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | incident_c(f13(A,B,D),A) | incident_c(f14(A,B,D),D). [assumption]. given #53 (I,wt=26): 87 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | -incident_c(f14(A,B,D),A). [assumption]. given #54 (I,wt=26): 88 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),B) | incident_c(f14(A,B,D),D). [assumption]. given #55 (I,wt=26): 89 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | -incident_c(f14(A,B,D),A). [assumption]. given #56 (I,wt=26): 90 incident_c(f12(A,B),B) | incident_c(C,B) | incident_c(C,D) | -incident_c(C,A) | -incident_c(f13(A,B,D),D) | incident_c(f14(A,B,D),D). [assumption]. given #57 (I,wt=11): 91 end_point(A,B) | -incident_c(A,B) | part_of(f15(A,B),B). [assumption]. given #58 (I,wt=11): 92 end_point(A,B) | -incident_c(A,B) | incident_c(A,f15(A,B)). [assumption]. given #59 (I,wt=11): 93 end_point(A,B) | -incident_c(A,B) | part_of(f16(A,B),B). [assumption]. given #60 (I,wt=11): 94 end_point(A,B) | -incident_c(A,B) | incident_c(A,f16(A,B)). [assumption]. given #61 (I,wt=13): 95 end_point(A,B) | -incident_c(A,B) | -part_of(f15(A,B),f16(A,B)). [assumption]. given #62 (I,wt=13): 96 end_point(A,B) | -incident_c(A,B) | -part_of(f16(A,B),f15(A,B)). [assumption]. given #63 (I,wt=6): 97 incident_c(A,B) | -end_point(A,B). [assumption]. given #64 (I,wt=21): 98 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -end_point(C,B). [assumption]. given #65 (I,wt=26): 99 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f17(C,B),B). [assumption]. given #66 (I,wt=26): 100 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f17(C,B)). [assumption]. given #67 (I,wt=26): 101 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | part_of(f18(C,B),B). [assumption]. given #68 (I,wt=26): 102 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | incident_c(C,f18(C,B)). [assumption]. given #69 (I,wt=28): 103 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f17(C,B),f18(C,B)). [assumption]. given #70 (I,wt=28): 104 -part_of(A,B) | -incident_c(C,A) | -part_of(D,B) | -incident_c(C,D) | part_of(A,D) | part_of(D,A) | -incident_c(C,B) | -part_of(f18(C,B),f17(C,B)). [assumption]. given #71 (I,wt=9): 105 inner_point(A,B) | -incident_c(A,B) | end_point(A,B). [assumption]. given #72 (I,wt=6): 106 incident_c(A,B) | -inner_point(A,B). [assumption]. given #73 (I,wt=6): 107 -end_point(A,B) | -inner_point(A,B). [assumption]. given #74 (I,wt=22): 108 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. given #75 (I,wt=22): 109 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. given #76 (I,wt=22): 110 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. given #77 (I,wt=22): 111 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),B). [assumption]. given #78 (I,wt=22): 112 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | incident_c(f20(A,B,C),C). [assumption]. given #79 (I,wt=22): 113 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | incident_c(f19(A,B,C),C) | -end_point(f20(A,B,C),C). [assumption]. given #80 (I,wt=22): 114 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),B). [assumption]. given #81 (I,wt=22): 115 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | incident_c(f20(A,B,C),C). [assumption]. given #82 (I,wt=22): 116 -incident_c(A,B) | meet(A,B,C) | -incident_c(A,C) | -end_point(f19(A,B,C),B) | -end_point(f20(A,B,C),C). [assumption]. given #83 (I,wt=7): 117 incident_c(A,B) | -meet(A,B,C). [assumption]. given #84 (I,wt=7): 118 incident_c(A,B) | -meet(A,C,B). [assumption]. given #85 (I,wt=13): 119 -incident_c(A,B) | -incident_c(A,C) | end_point(A,B) | -meet(D,B,C). [assumption]. given #86 (I,wt=27): 120 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. given #87 (I,wt=27): 121 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. given #88 (I,wt=27): 122 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. given #89 (I,wt=27): 123 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),B). [assumption]. given #90 (I,wt=27): 124 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | incident_c(f22(A,B,D),D). [assumption]. given #91 (I,wt=27): 125 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | incident_c(f21(A,B,D),D) | -end_point(f22(A,B,D),D). [assumption]. given #92 (I,wt=27): 126 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),B). [assumption]. given #93 (I,wt=27): 127 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | incident_c(f22(A,B,D),D). [assumption]. given #94 (I,wt=27): 128 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,B) | -incident_c(A,D) | -end_point(f21(A,B,D),B) | -end_point(f22(A,B,D),D). [assumption]. given #95 (I,wt=13): 129 -incident_c(A,B) | -incident_c(A,C) | end_point(A,C) | -meet(D,B,C). [assumption]. given #96 (I,wt=27): 130 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. given #97 (I,wt=27): 131 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. given #98 (I,wt=27): 132 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. given #99 (I,wt=27): 133 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),B). [assumption]. given #100 (I,wt=27): 134 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | incident_c(f24(A,B,D),D). [assumption]. given #101 (I,wt=27): 135 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | incident_c(f23(A,B,D),D) | -end_point(f24(A,B,D),D). [assumption]. given #102 (I,wt=27): 136 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),B). [assumption]. given #103 (I,wt=27): 137 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | incident_c(f24(A,B,D),D). [assumption]. given #104 (I,wt=27): 138 -incident_c(A,B) | -incident_c(C,B) | -incident_c(C,D) | end_point(C,D) | -incident_c(A,D) | -end_point(f23(A,B,D),B) | -end_point(f24(A,B,D),D). [assumption]. given #105 (I,wt=7): 139 -end_point(A,B) | end_point(f26(B),B). [assumption]. given #106 (I,wt=7): 140 end_point(f28(A),A) | -end_point(B,A). [assumption]. given #107 (I,wt=36): 141 -part_of(A,B) | -part_of(C,B) | part_of(A,C) | part_of(C,A) | -part_of(D,B) | -end_point(E,A) | -end_point(E,C) | -end_point(E,D) | part_of(C,D) | part_of(D,C) | part_of(A,D) | part_of(D,A). [assumption]. given #108 (I,wt=4): 142 inner_point(f29(A),A). [assumption]. given #109 (I,wt=11): 143 -inner_point(A,B) | meet(A,f30(B,A),f31(B,A)). [assumption]. given #110 (I,wt=12): 144 -inner_point(A,B) | sum(f30(B,A),f31(B,A)) = B. [assumption]. given #111 (I,wt=18): 145 -end_point(A,B) | -end_point(C,B) | C = A | -end_point(D,B) | D = A | D = C. [assumption]. given #112 (I,wt=8): 146 -end_point(A,B) | end_point(f32(B,A),B). [assumption]. given #113 (I,wt=8): 147 -end_point(A,B) | f32(B,A) != A. [assumption]. given #114 (I,wt=11): 149 -meet(A,B,C) | f33(B,C) = sum(B,C). [copy(148),flip(b)]. given #115 (I,wt=13): 150 incident_c(f34(A,B),A) | -incident_c(f35(A,B),A) | B = A. [assumption]. given #116 (I,wt=13): 151 incident_c(f34(A,B),A) | incident_c(f35(A,B),B) | B = A. [assumption]. given #117 (I,wt=13): 152 -incident_c(f34(A,B),B) | -incident_c(f35(A,B),A) | B = A. [assumption]. given #118 (I,wt=13): 153 -incident_c(f34(A,B),B) | incident_c(f35(A,B),B) | B = A. [assumption]. given #119 (I,wt=20): 154 between_c(A,B,C,D) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. given #120 (I,wt=8): 155 A != B | -between_c(C,B,D,A). [assumption]. given #121 (I,wt=12): 156 part_of(f36(A,B,C,D),A) | -between_c(A,B,C,D). [assumption]. given #122 (I,wt=12): 157 end_point(A,f36(B,A,C,D)) | -between_c(B,A,C,D). [assumption]. given #123 (I,wt=12): 158 end_point(A,f36(B,C,D,A)) | -between_c(B,C,D,A). [assumption]. given #124 (I,wt=12): 159 inner_point(A,f36(B,C,A,D)) | -between_c(B,C,A,D). [assumption]. given #125 (I,wt=22): 160 part_of(f37(A,B,C,D),A) | D = B | -part_of(E,A) | -end_point(B,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. given #126 (I,wt=22): 161 end_point(A,f37(B,A,C,D)) | D = A | -part_of(E,B) | -end_point(A,E) | -end_point(D,E) | -inner_point(C,E). [assumption]. given #127 (I,wt=22): 162 end_point(A,f37(B,C,D,A)) | A = C | -part_of(E,B) | -end_point(C,E) | -end_point(A,E) | -inner_point(D,E). [assumption]. given #128 (I,wt=22): 163 inner_point(A,f37(B,C,A,D)) | D = C | -part_of(E,B) | -end_point(C,E) | -end_point(D,E) | -inner_point(A,E). [assumption]. given #129 (I,wt=18): 164 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f39(B,C) != B. [assumption]. given #130 (I,wt=18): 165 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f39(B,C),C). [assumption]. given #131 (I,wt=19): 166 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f39(B,C)). [assumption]. given #132 (I,wt=18): 167 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f41(B,C) != B. [assumption]. given #133 (I,wt=18): 168 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f41(B,C),C). [assumption]. given #134 (I,wt=19): 169 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f41(B,C),B). [assumption]. given #135 (I,wt=7): 170 incident_o(A,B) | -ordered_by(B,A,C). [assumption]. given #136 (I,wt=7): 171 -ordered_by(A,B,C) | incident_o(C,A). [assumption]. given #137 (I,wt=7): 172 incident_o(A,B) | -incident_c(A,f42(B)). [assumption]. given #138 (I,wt=7): 173 incident_c(A,f42(B)) | -incident_o(A,B). [assumption]. given #139 (I,wt=31): 174 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. given #140 (I,wt=31): 175 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | incident_o(f47(C,D,E,B,F),B) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. given #141 (I,wt=31): 176 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | -incident_o(f48(C,D,E,B,F),B) | -between_c(F,C,D,E). [assumption]. given #142 (I,wt=31): 177 incident_o(A,B) | -incident_c(A,f46(C,D,E,B)) | -incident_c(f47(C,D,E,B,F),F) | incident_c(f48(C,D,E,B,F),F) | -between_c(F,C,D,E). [assumption]. given #143 (I,wt=31): 178 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. given #144 (I,wt=31): 179 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | incident_o(f47(B,C,D,E,F),E) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. given #145 (I,wt=31): 180 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | -incident_o(f48(B,C,D,E,F),E) | -between_c(F,B,C,D). [assumption]. given #146 (I,wt=31): 181 incident_c(A,f46(B,C,D,E)) | -incident_o(A,E) | -incident_c(f47(B,C,D,E,F),F) | incident_c(f48(B,C,D,E,F),F) | -between_c(F,B,C,D). [assumption]. given #147 (I,wt=30): 182 between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. given #148 (I,wt=30): 183 between_c(f46(A,B,C,D),A,B,C) | incident_o(f47(A,B,C,D,E),D) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. given #149 (I,wt=30): 184 between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | -incident_o(f48(A,B,C,D,E),D) | -between_c(E,A,B,C). [assumption]. given #150 (I,wt=30): 185 between_c(f46(A,B,C,D),A,B,C) | -incident_c(f47(A,B,C,D,E),E) | incident_c(f48(A,B,C,D,E),E) | -between_c(E,A,B,C). [assumption]. given #151 (I,wt=19): 186 ordered_by(A,f51(A,B),f52(A,B)) | -ordered_by(A,f53(A,B),f54(A,B)) | B = A. [assumption]. given #152 (I,wt=19): 187 ordered_by(A,f51(A,B),f52(A,B)) | ordered_by(B,f53(A,B),f54(A,B)) | B = A. [assumption]. given #153 (I,wt=19): 188 -ordered_by(A,f51(B,A),f52(B,A)) | -ordered_by(B,f53(B,A),f54(B,A)) | A = B. [assumption]. given #154 (I,wt=19): 189 -ordered_by(A,f51(B,A),f52(B,A)) | ordered_by(A,f53(B,A),f54(B,A)) | A = B. [assumption]. given #155 (I,wt=14): 190 underlying_curve(A) = B | incident_o(f55(B,A),A) | -incident_o(f56(B,A),A). [assumption]. given #156 (I,wt=14): 191 underlying_curve(A) = B | incident_o(f55(B,A),A) | incident_c(f56(B,A),B). [assumption]. given #157 (I,wt=14): 192 underlying_curve(A) = B | -incident_c(f55(B,A),B) | -incident_o(f56(B,A),A). [assumption]. given #158 (I,wt=14): 193 underlying_curve(A) = B | -incident_c(f55(B,A),B) | incident_c(f56(B,A),B). [assumption]. given #159 (I,wt=10): 194 incident_o(A,B) | -incident_c(A,C) | underlying_curve(B) != C. [assumption]. given #160 (I,wt=16): 195 incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | -incident_o(f58(C,B),B). [assumption]. given #161 (I,wt=16): 196 incident_o(A,B) | -incident_c(A,C) | incident_o(f57(C,B),B) | incident_c(f58(C,B),C). [assumption]. given #162 (I,wt=16): 197 incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | -incident_o(f58(C,B),B). [assumption]. given #163 (I,wt=16): 198 incident_o(A,B) | -incident_c(A,C) | -incident_c(f57(C,B),C) | incident_c(f58(C,B),C). [assumption]. given #164 (I,wt=10): 199 incident_c(A,B) | -incident_o(A,C) | underlying_curve(C) != B. [assumption]. given #165 (I,wt=16): 200 incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | -incident_o(f60(B,C),C). [assumption]. given #166 (I,wt=16): 201 incident_c(A,B) | -incident_o(A,C) | incident_o(f59(B,C),C) | incident_c(f60(B,C),B). [assumption]. given #167 (I,wt=16): 202 incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | -incident_o(f60(B,C),C). [assumption]. given #168 (I,wt=16): 203 incident_c(A,B) | -incident_o(A,C) | -incident_c(f59(B,C),B) | incident_c(f60(B,C),B). [assumption]. given #169 (I,wt=12): 204 connect(A,B,C) | -once(at_the_same_time(at(A,C),at(B,C))). [assumption]. given #170 (I,wt=12): 205 once(at_the_same_time(at(A,B),at(C,B))) | -connect(A,C,B). [assumption]. given #171 (I,wt=8): 206 once(at_the_same_time(A,B)) | -once(at_the_same_time(B,A)). [assumption]. given #172 (I,wt=12): 207 once(at_the_same_time(at_the_same_time(A,B),C)) | -once(at_the_same_time(A,at_the_same_time(B,C))). [assumption]. given #173 (I,wt=12): 208 once(at_the_same_time(A,at_the_same_time(B,C))) | -once(at_the_same_time(at_the_same_time(A,B),C)). [assumption]. given #174 (I,wt=6): 209 -once(A) | once(at_the_same_time(A,A)). [assumption]. given #175 (I,wt=6): 210 once(A) | -once(at_the_same_time(A,B)). [assumption]. given #176 (I,wt=6): 211 -once(at_the_same_time(A,B)) | once(B). [assumption]. given #177 (I,wt=5): 214 trajectory_of(A) = f61(A). [assumption]. given #178 (I,wt=26): 216 -ordered_by(f61(A),B,C) | -once(at_the_same_time(at(A,B),at(D,E))) | -once(at_the_same_time(at(A,C),at(D,F))) | -ordered_by(f61(D),F,E). [copy(215),rewrite(214(1),214(11))]. given #179 (I,wt=10): 217 -once(A) | once(at_the_same_time(A,at(B,f62(A,B)))). [assumption]. given #180 (I,wt=4): 218 connect(c1,c2,c3). [assumption]. given #181 (I,wt=4): 219 -connect(c2,c1,c3). [assumption]. given #182 (I,wt=7): 220 -end_point(A,B) | end_point(f25(B),B). [resolve(1,b,2,a)]. given #183 (I,wt=20): 221 sum(A,B) != C | -end_point(D,A) | meet(D,A,B) | -meet(E,A,B) | end_point(f25(C),C). [resolve(3,a,2,a)]. given #184 (I,wt=7): 222 end_point(f27(A),A) | -end_point(B,A). [resolve(4,b,5,a)]. given #185 (I,wt=10): 223 -part_of(A,B) | A = B | end_point(f27(A),A). [resolve(6,c,4,b)]. given #186 (I,wt=6): 224 end_point(f27(f42(A)),f42(A)). [resolve(7,a,4,b)]. given #187 (I,wt=21): 225 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -end_point(E,C). [resolve(8,b,5,a)]. given #188 (I,wt=24): 226 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_o(D,f50(B,A,C)) | -incident_c(D,C) | -part_of(C,E) | C = E. [resolve(8,b,6,c)]. given #189 (I,wt=22): 227 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_o(D,f50(B,A,f42(C))) | -incident_c(D,f42(C)). [resolve(8,b,7,a)]. given #190 (I,wt=21): 228 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -end_point(E,C). [resolve(9,b,5,a)]. given #191 (I,wt=24): 229 A = B | -incident_c(B,C) | -incident_c(A,C) | incident_c(D,C) | -incident_o(D,f50(B,A,C)) | -part_of(C,E) | C = E. [resolve(9,b,6,c)]. given #192 (I,wt=22): 230 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | incident_c(D,f42(C)) | -incident_o(D,f50(B,A,f42(C))). [resolve(9,b,7,a)]. given #193 (I,wt=19): 231 A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -end_point(D,C). [resolve(10,b,5,a)]. given #194 (I,wt=22): 232 A = B | -incident_c(B,C) | -incident_c(A,C) | ordered_by(f50(B,A,C),B,A) | -part_of(C,D) | C = D. [resolve(10,b,6,c)]. given #195 (I,wt=19): 233 A = B | -incident_c(B,f42(C)) | -incident_c(A,f42(C)) | ordered_by(f50(B,A,f42(C)),B,A). [resolve(10,b,7,a)]. given #196 (I,wt=29): 234 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(17,a,11,c)]. given #197 (I,wt=29): 235 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(17,a,14,c)]. given #198 (I,wt=29): 236 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(17,a,15,c)]. given #199 (I,wt=29): 237 incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(17,a,16,c)]. given #200 (I,wt=29): 238 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(18,a,11,c)]. given #201 (I,wt=29): 239 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(18,a,14,c)]. given #202 (I,wt=29): 240 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(18,a,15,c)]. given #203 (I,wt=29): 241 incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(18,a,16,c)]. given #204 (I,wt=29): 242 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(19,a,11,c)]. given #205 (I,wt=29): 243 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(19,a,14,c)]. given #206 (I,wt=29): 244 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(19,a,15,c)]. given #207 (I,wt=29): 245 -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(19,a,16,c)]. given #208 (I,wt=29): 246 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,C,B). [resolve(20,a,11,c)]. given #209 (I,wt=29): 247 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,A,B) | ordered_by(D,B,A). [resolve(20,a,14,c)]. given #210 (I,wt=29): 248 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,C) | ordered_by(D,C,B). [resolve(20,a,15,c)]. given #211 (I,wt=29): 249 -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C) | ordered_by(D,B,A) | ordered_by(D,B,C). [resolve(20,a,16,c)]. given #212 (I,wt=18): 250 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,C,D) | -ordered_by(B,D,E). [resolve(21,c,12,b)]. given #213 (I,wt=18): 251 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -ordered_by(B,D,C) | -ordered_by(B,E,D). [resolve(21,c,13,b)]. given #214 (I,wt=31): 252 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,17,a)]. given #215 (I,wt=31): 253 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | incident_o(f43(C,D,E,B,F),B) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,18,a)]. given #216 (I,wt=31): 254 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | -incident_o(f44(C,D,E,B,F),B) | -between_c(F,C,D,E). [resolve(21,c,19,a)]. given #217 (I,wt=31): 255 incident_o(A,B) | -incident_c(A,f45(C,D,E,B)) | -incident_c(f43(C,D,E,B,F),F) | incident_c(f44(C,D,E,B,F),F) | -between_c(F,C,D,E). [resolve(21,c,20,a)]. given #218 (I,wt=18): 256 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,B,C) | -ordered_by(E,C,D). [resolve(22,c,12,b)]. given #219 (I,wt=18): 257 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -ordered_by(E,C,B) | -ordered_by(E,D,C). [resolve(22,c,13,b)]. given #220 (I,wt=31): 258 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,17,a)]. given #221 (I,wt=31): 259 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | incident_o(f43(B,C,D,E,F),E) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,18,a)]. given #222 (I,wt=31): 260 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | -incident_o(f44(B,C,D,E,F),E) | -between_c(F,B,C,D). [resolve(22,c,19,a)]. given #223 (I,wt=31): 261 incident_c(A,f45(B,C,D,E)) | -incident_o(A,E) | -incident_c(f43(B,C,D,E,F),F) | incident_c(f44(B,C,D,E,F),F) | -between_c(F,B,C,D). [resolve(22,c,20,a)]. given #224 (I,wt=17): 262 between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,A,B) | -ordered_by(D,B,C). [resolve(23,b,12,b)]. given #225 (I,wt=17): 263 between_c(f45(A,B,C,D),A,B,C) | -ordered_by(D,B,A) | -ordered_by(D,C,B). [resolve(23,b,13,b)]. given #226 (I,wt=30): 264 between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,17,a)]. given #227 (I,wt=30): 265 between_c(f45(A,B,C,D),A,B,C) | incident_o(f43(A,B,C,D,E),D) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,18,a)]. given #228 (I,wt=30): 266 between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | -incident_o(f44(A,B,C,D,E),D) | -between_c(E,A,B,C). [resolve(23,b,19,a)]. given #229 (I,wt=30): 267 between_c(f45(A,B,C,D),A,B,C) | -incident_c(f43(A,B,C,D,E),E) | incident_c(f44(A,B,C,D,E),E) | -between_c(E,A,B,C). [resolve(23,b,20,a)]. given #230 (I,wt=18): 268 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | f38(B,C) != B. [resolve(28,d,25,a)]. given #231 (I,wt=18): 269 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | incident_o(f38(B,C),C). [resolve(28,d,26,a)]. given #232 (I,wt=19): 270 A = B | -incident_o(A,C) | ordered_by(C,B,A) | -incident_o(B,C) | -ordered_by(C,B,f38(B,C)). [resolve(28,d,27,a)]. given #233 (I,wt=4): 271 incident_o(f49(A),A). [resolve(29,a,24,b)]. given #234 (I,wt=12): 273 f49(A) = B | -incident_o(B,A) | ordered_by(A,f49(A),B). [copy(272),flip(a)]. given #235 (I,wt=18): 274 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | f40(B,C) != B. [resolve(34,d,31,a)]. given #236 (I,wt=18): 275 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | incident_o(f40(B,C),C). [resolve(34,d,32,a)]. given #237 (I,wt=19): 276 A = B | -incident_o(A,C) | ordered_by(C,A,B) | -incident_o(B,C) | -ordered_by(C,f40(B,C),B). [resolve(34,d,33,a)]. given #238 (I,wt=23): 277 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | -incident_c(f6(A,B),A) | -incident_c(f8(A,B,C),A). [factor(53,a,d)]. given #239 (I,wt=23): 278 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | -incident_c(f6(A,B),A) | incident_c(f8(A,B,C),C). [factor(54,a,d)]. given #240 (I,wt=23): 279 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | incident_c(f7(A,B,A),A). [factor(54,a,e)]. given #241 (I,wt=23): 280 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | -incident_c(f7(A,B,A),B). [factor(56,a,e)]. given #242 (I,wt=23): 281 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | -incident_c(f6(A,B),A) | -incident_c(f7(A,B,A),A). [factor(58,a,e)]. given #243 (I,wt=23): 282 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | incident_c(f6(A,B),B) | -incident_c(f8(A,B,C),A). [factor(59,a,d)]. given #244 (I,wt=23): 283 incident_c(f7(A,B,C),A) | -incident_c(f7(A,B,C),B) | incident_c(f6(A,B),B) | incident_c(f8(A,B,C),C). [factor(60,a,d)]. given #245 (I,wt=23): 284 incident_c(f8(A,B,A),A) | -incident_c(f8(A,B,A),B) | incident_c(f6(A,B),B)