%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET055-6 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:20:20 EDT 2024
% Result : Unsatisfiable 14.79s 14.91s
% Output : CNFRefutation 14.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : SET055-6 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.30 % Computer : n027.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Sun Jun 23 17:12:54 EDT 2024
% 0.09/0.30 % CPUTime :
% 0.16/0.55 start to proof:theBenchmark
% 14.74/14.87 %-------------------------------------------
% 14.74/14.87 % File :CSE---1.7
% 14.74/14.87 % Problem :theBenchmark
% 14.74/14.87 % Transform :cnf
% 14.74/14.87 % Format :tptp:raw
% 14.74/14.87 % Command :java -jar mcs_scs.jar %d %s
% 14.74/14.87
% 14.74/14.87 % Result :Theorem 14.240000s
% 14.74/14.87 % Output :CNFRefutation 14.240000s
% 14.74/14.87 %-------------------------------------------
% 14.79/14.88 %--------------------------------------------------------------------------
% 14.79/14.88 % File : SET055-6 : TPTP v8.2.0. Released v1.0.0.
% 14.79/14.88 % Domain : Set Theory
% 14.79/14.88 % Problem : Equality is reflexive
% 14.79/14.88 % Version : [Qua92] axioms.
% 14.79/14.88 % English :
% 14.79/14.88
% 14.79/14.88 % Refs : [Qua92] Quaife (1992), Automated Deduction in von Neumann-Bern
% 14.79/14.88 % Source : [Quaife]
% 14.79/14.88 % Names :
% 14.79/14.88
% 14.79/14.88 % Status : Unsatisfiable
% 14.79/14.88 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.4.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.29 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.1.0, 0.12 v2.0.0
% 14.79/14.88 % Syntax : Number of clauses : 159 ( 30 unt; 8 nHn; 94 RR)
% 14.79/14.88 % Number of literals : 332 ( 0 equ; 168 neg)
% 14.79/14.88 % Maximal clause size : 5 ( 2 avg)
% 14.79/14.88 % Maximal term depth : 6 ( 1 avg)
% 14.79/14.88 % Number of predicates : 10 ( 10 usr; 0 prp; 1-3 aty)
% 14.79/14.88 % Number of functors : 39 ( 39 usr; 9 con; 0-3 aty)
% 14.79/14.88 % Number of variables : 378 ( 26 sgn)
% 14.79/14.88 % SPC : CNF_UNS_RFO_NEQ_NHN
% 14.79/14.88
% 14.79/14.88 % Comments :
% 14.79/14.88 %--------------------------------------------------------------------------
% 14.79/14.88 %----Don't include von Neuman-Bernays-Godel set theory axioms because
% 14.79/14.88 %----equality is incomplete
% 14.79/14.88 %include('Axioms/SET004-0.ax').
% 14.79/14.88 %--------------------------------------------------------------------------
% 14.79/14.88 cnf(symmetry,axiom,
% 14.79/14.88 ( ~ equalish(X,Y)
% 14.79/14.88 | equalish(Y,X) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(transitivity,axiom,
% 14.79/14.88 ( ~ equalish(X,Y)
% 14.79/14.88 | ~ equalish(Y,Z)
% 14.79/14.88 | equalish(X,Z) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(apply_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(D,E)
% 14.79/14.88 | equalish(apply(D,F),apply(E,F)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(apply_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(G,H)
% 14.79/14.88 | equalish(apply(I,G),apply(I,H)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(cantor_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(J,K)
% 14.79/14.88 | equalish(cantor(J),cantor(K)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(complement_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L,M)
% 14.79/14.88 | equalish(complement(L),complement(M)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(compose_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(N,O)
% 14.79/14.88 | equalish(compose(N,P),compose(O,P)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(compose_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(Q,R)
% 14.79/14.88 | equalish(compose(S,Q),compose(S,R)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(cross_product_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(T,U)
% 14.79/14.88 | equalish(cross_product(T,V),cross_product(U,V)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(cross_product_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(W,X)
% 14.79/14.88 | equalish(cross_product(Y,W),cross_product(Y,X)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(diagonalise_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(Z,A1)
% 14.79/14.88 | equalish(diagonalise(Z),diagonalise(A1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(symmetric_difference_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(B1,C1)
% 14.79/14.88 | equalish(symmetric_difference(B1,D1),symmetric_difference(C1,D1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(symmetric_difference_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(E1,F1)
% 14.79/14.88 | equalish(symmetric_difference(G1,E1),symmetric_difference(G1,F1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(domain_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(H1,I1)
% 14.79/14.88 | equalish(domain(H1,J1,K1),domain(I1,J1,K1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(domain_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(L1,M1)
% 14.79/14.88 | equalish(domain(N1,L1,O1),domain(N1,M1,O1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(domain_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(P1,Q1)
% 14.79/14.88 | equalish(domain(R1,S1,P1),domain(R1,S1,Q1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(domain_of_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(T1,U1)
% 14.79/14.88 | equalish(domain_of(T1),domain_of(U1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(first_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(V1,W1)
% 14.79/14.88 | equalish(first(V1),first(W1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(flip_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(X1,Y1)
% 14.79/14.88 | equalish(flip(X1),flip(Y1)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(image_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(Z1,A2)
% 14.79/14.88 | equalish(image(Z1,B2),image(A2,B2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(image_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(C2,D2)
% 14.79/14.88 | equalish(image(E2,C2),image(E2,D2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(intersection_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(F2,G2)
% 14.79/14.88 | equalish(intersection(F2,H2),intersection(G2,H2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(intersection_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(I2,J2)
% 14.79/14.88 | equalish(intersection(K2,I2),intersection(K2,J2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(inverse_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L2,M2)
% 14.79/14.88 | equalish(inverse(L2),inverse(M2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism1_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(N2,O2)
% 14.79/14.88 | equalish(not_homomorphism1(N2,P2,Q2),not_homomorphism1(O2,P2,Q2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism1_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(R2,S2)
% 14.79/14.88 | equalish(not_homomorphism1(T2,R2,U2),not_homomorphism1(T2,S2,U2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism1_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(V2,W2)
% 14.79/14.88 | equalish(not_homomorphism1(X2,Y2,V2),not_homomorphism1(X2,Y2,W2)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism2_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(Z2,A3)
% 14.79/14.88 | equalish(not_homomorphism2(Z2,B3,C3),not_homomorphism2(A3,B3,C3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism2_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(D3,E3)
% 14.79/14.88 | equalish(not_homomorphism2(F3,D3,G3),not_homomorphism2(F3,E3,G3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_homomorphism2_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(H3,I3)
% 14.79/14.88 | equalish(not_homomorphism2(J3,K3,H3),not_homomorphism2(J3,K3,I3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_subclass_element_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L3,M3)
% 14.79/14.88 | equalish(not_subclass_element(L3,N3),not_subclass_element(M3,N3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(not_subclass_element_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(O3,P3)
% 14.79/14.88 | equalish(not_subclass_element(Q3,O3),not_subclass_element(Q3,P3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(ordered_pair_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(R3,S3)
% 14.79/14.88 | equalish(ordered_pair(R3,T3),ordered_pair(S3,T3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(ordered_pair_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(U3,V3)
% 14.79/14.88 | equalish(ordered_pair(W3,U3),ordered_pair(W3,V3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(power_class_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(X3,Y3)
% 14.79/14.88 | equalish(power_class(X3),power_class(Y3)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(range_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(Z3,A4)
% 14.79/14.88 | equalish(range(Z3,B4,C4),range(A4,B4,C4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(range_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(D4,E4)
% 14.79/14.88 | equalish(range(F4,D4,G4),range(F4,E4,G4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(range_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(H4,I4)
% 14.79/14.88 | equalish(range(J4,K4,H4),range(J4,K4,I4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(range_of_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L4,M4)
% 14.79/14.88 | equalish(range_of(L4),range_of(M4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(regular_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(N4,O4)
% 14.79/14.88 | equalish(regular(N4),regular(O4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(restrict_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(P4,Q4)
% 14.79/14.88 | equalish(restrict(P4,R4,S4),restrict(Q4,R4,S4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(restrict_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(T4,U4)
% 14.79/14.88 | equalish(restrict(V4,T4,W4),restrict(V4,U4,W4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(restrict_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(X4,Y4)
% 14.79/14.88 | equalish(restrict(Z4,A5,X4),restrict(Z4,A5,Y4)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(rotate_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(B5,C5)
% 14.79/14.88 | equalish(rotate(B5),rotate(C5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(second_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(D5,E5)
% 14.79/14.88 | equalish(second(D5),second(E5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(singleton_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(F5,G5)
% 14.79/14.88 | equalish(singleton(F5),singleton(G5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(successor_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(H5,I5)
% 14.79/14.88 | equalish(successor(H5),successor(I5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(sum_class_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(J5,K5)
% 14.79/14.88 | equalish(sum_class(J5),sum_class(K5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(union_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L5,M5)
% 14.79/14.88 | equalish(union(L5,N5),union(M5,N5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(union_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(O5,P5)
% 14.79/14.88 | equalish(union(Q5,O5),union(Q5,P5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(unordered_pair_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(R5,S5)
% 14.79/14.88 | equalish(unordered_pair(R5,T5),unordered_pair(S5,T5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(unordered_pair_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(U5,V5)
% 14.79/14.88 | equalish(unordered_pair(W5,U5),unordered_pair(W5,V5)) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(compatible_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(X5,Y5)
% 14.79/14.88 | ~ compatible(X5,Z5,A6)
% 14.79/14.88 | compatible(Y5,Z5,A6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(compatible_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(B6,C6)
% 14.79/14.88 | ~ compatible(D6,B6,E6)
% 14.79/14.88 | compatible(D6,C6,E6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(compatible_substitution3,axiom,
% 14.79/14.88 ( ~ equalish(F6,G6)
% 14.79/14.88 | ~ compatible(H6,I6,F6)
% 14.79/14.88 | compatible(H6,I6,G6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(function_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(J6,K6)
% 14.79/14.88 | ~ function(J6)
% 14.79/14.88 | function(K6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(homomorphism_substitution1,axiom,
% 14.79/14.88 ( ~ equalish(L6,M6)
% 14.79/14.88 | ~ homomorphism(L6,N6,O6)
% 14.79/14.88 | homomorphism(M6,N6,O6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(homomorphism_substitution2,axiom,
% 14.79/14.88 ( ~ equalish(P6,Q6)
% 14.79/14.88 | ~ homomorphism(R6,P6,S6)
% 14.79/14.88 | homomorphism(R6,Q6,S6) ) ).
% 14.79/14.88
% 14.79/14.88 cnf(homomorphism_substitution3,axiom,
% 14.79/14.89 ( ~ equalish(T6,U6)
% 14.79/14.89 | ~ homomorphism(V6,W6,T6)
% 14.79/14.89 | homomorphism(V6,W6,U6) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(inductive_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(X6,Y6)
% 14.79/14.89 | ~ inductive(X6)
% 14.79/14.89 | inductive(Y6) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(member_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(Z6,A7)
% 14.79/14.89 | ~ member(Z6,B7)
% 14.79/14.89 | member(A7,B7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(member_substitution2,axiom,
% 14.79/14.89 ( ~ equalish(C7,D7)
% 14.79/14.89 | ~ member(E7,C7)
% 14.79/14.89 | member(E7,D7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(one_to_one_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(F7,G7)
% 14.79/14.89 | ~ one_to_one(F7)
% 14.79/14.89 | one_to_one(G7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(operation_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(H7,I7)
% 14.79/14.89 | ~ operation(H7)
% 14.79/14.89 | operation(I7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(single_valued_class_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(J7,K7)
% 14.79/14.89 | ~ single_valued_class(J7)
% 14.79/14.89 | single_valued_class(K7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(subclass_substitution1,axiom,
% 14.79/14.89 ( ~ equalish(L7,M7)
% 14.79/14.89 | ~ subclass(L7,N7)
% 14.79/14.89 | subclass(M7,N7) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(subclass_substitution2,axiom,
% 14.79/14.89 ( ~ equalish(O7,P7)
% 14.79/14.89 | ~ subclass(Q7,O7)
% 14.79/14.89 | subclass(Q7,P7) ) ).
% 14.79/14.89
% 14.79/14.89 %----GROUP 1: AXIOMS AND BASIC DEFINITIONS.
% 14.79/14.89
% 14.79/14.89 %----Axiom A-1: sets are classes (omitted because all objects are
% 14.79/14.89 %----classes).
% 14.79/14.89
% 14.79/14.89 %----Definition of < (subclass).
% 14.79/14.89 %----a:x:a:y:((x < y) <=> a:u:((u e x) ==> (u e y))).
% 14.79/14.89 cnf(subclass_members,axiom,
% 14.79/14.89 ( ~ subclass(X,Y)
% 14.79/14.89 | ~ member(U,X)
% 14.79/14.89 | member(U,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(not_subclass_members1,axiom,
% 14.79/14.89 ( member(not_subclass_element(X,Y),X)
% 14.79/14.89 | subclass(X,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(not_subclass_members2,axiom,
% 14.79/14.89 ( ~ member(not_subclass_element(X,Y),Y)
% 14.79/14.89 | subclass(X,Y) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom A-2: elements of classes are sets.
% 14.79/14.89 %----a:x:(x < universal_class).
% 14.79/14.89 cnf(class_elements_are_sets,axiom,
% 14.79/14.89 subclass(X,universal_class) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom A-3: principle of extensionality.
% 14.79/14.89 %----a:x:a:y:((x = y) <=> (x < y) & (y < x)).
% 14.79/14.89 cnf(equal_implies_subclass1,axiom,
% 14.79/14.89 ( ~ equalish(X,Y)
% 14.79/14.89 | subclass(X,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(equal_implies_subclass2,axiom,
% 14.79/14.89 ( ~ equalish(X,Y)
% 14.79/14.89 | subclass(Y,X) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(subclass_implies_equal,axiom,
% 14.79/14.89 ( ~ subclass(X,Y)
% 14.79/14.89 | ~ subclass(Y,X)
% 14.79/14.89 | equalish(X,Y) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom A-4: existence of unordered pair.
% 14.79/14.89 %----a:u:a:x:a:y:((u e {x, y}) <=> (u e universal_class)
% 14.79/14.89 %----& (u = x | u = y)).
% 14.79/14.89 %----a:x:a:y:({x, y} e universal_class).
% 14.79/14.89 cnf(unordered_pair_member,axiom,
% 14.79/14.89 ( ~ member(U,unordered_pair(X,Y))
% 14.79/14.89 | equalish(U,X)
% 14.79/14.89 | equalish(U,Y) ) ).
% 14.79/14.89
% 14.79/14.89 %----(x e universal_class), (u = x) --> (u e {x, y}).
% 14.79/14.89 cnf(unordered_pair2,axiom,
% 14.79/14.89 ( ~ member(X,universal_class)
% 14.79/14.89 | member(X,unordered_pair(X,Y)) ) ).
% 14.79/14.89
% 14.79/14.89 %----(y e universal_class), (u = y) --> (u e {x, y}).
% 14.79/14.89 cnf(unordered_pair3,axiom,
% 14.79/14.89 ( ~ member(Y,universal_class)
% 14.79/14.89 | member(Y,unordered_pair(X,Y)) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(unordered_pairs_in_universal,axiom,
% 14.79/14.89 member(unordered_pair(X,Y),universal_class) ).
% 14.79/14.89
% 14.79/14.89 %----Definition of singleton set.
% 14.79/14.89 %----a:x:({x} = {x, x}).
% 14.79/14.89 cnf(singleton_set,axiom,
% 14.79/14.89 equalish(unordered_pair(X,X),singleton(X)) ).
% 14.79/14.89
% 14.79/14.89 %----See Theorem (SS6) for memb.
% 14.79/14.89
% 14.79/14.89 %----Definition of ordered pair.
% 14.79/14.89 %----a:x:a:y:([x,y] = {{x}, {x, {y}}}).
% 14.79/14.89 cnf(ordered_pair,axiom,
% 14.79/14.89 equalish(unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),ordered_pair(X,Y)) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-5'a: Cartesian product.
% 14.79/14.89 %----a:u:a:v:a:y:(([u,v] e cross_product(x,y)) <=> (u e x) & (v e y)).
% 14.79/14.89 cnf(cartesian_product1,axiom,
% 14.79/14.89 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 14.79/14.89 | member(U,X) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(cartesian_product2,axiom,
% 14.79/14.89 ( ~ member(ordered_pair(U,V),cross_product(X,Y))
% 14.79/14.89 | member(V,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(cartesian_product3,axiom,
% 14.79/14.89 ( ~ member(U,X)
% 14.79/14.89 | ~ member(V,Y)
% 14.79/14.89 | member(ordered_pair(U,V),cross_product(X,Y)) ) ).
% 14.79/14.89
% 14.79/14.89 %----See Theorem (OP6) for 1st and 2nd.
% 14.79/14.89
% 14.79/14.89 %----Axiom B-5'b: Cartesian product.
% 14.79/14.89 %----a:z:(z e cross_product(x,y) --> ([first(z),second(z)] = z)
% 14.79/14.89 cnf(cartesian_product4,axiom,
% 14.79/14.89 ( ~ member(Z,cross_product(X,Y))
% 14.79/14.89 | equalish(ordered_pair(first(Z),second(Z)),Z) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-1: E (element relation).
% 14.79/14.89 %----(E < cross_product(universal_class,universal_class)).
% 14.79/14.89 %----a:x:a:y:(([x,y] e E) <=> ([x,y] e cross_product(universal_class,
% 14.79/14.89 %----universal_class)) (x e y)).
% 14.79/14.89 cnf(element_relation1,axiom,
% 14.79/14.89 subclass(element_relation,cross_product(universal_class,universal_class)) ).
% 14.79/14.89
% 14.79/14.89 cnf(element_relation2,axiom,
% 14.79/14.89 ( ~ member(ordered_pair(X,Y),element_relation)
% 14.79/14.89 | member(X,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(element_relation3,axiom,
% 14.79/14.89 ( ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
% 14.79/14.89 | ~ member(X,Y)
% 14.79/14.89 | member(ordered_pair(X,Y),element_relation) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-2: * (intersection).
% 14.79/14.89 %----a:z:a:x:a:y:((z e (x * y)) <=> (z e x) & (z e y)).
% 14.79/14.89 cnf(intersection1,axiom,
% 14.79/14.89 ( ~ member(Z,intersection(X,Y))
% 14.79/14.89 | member(Z,X) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(intersection2,axiom,
% 14.79/14.89 ( ~ member(Z,intersection(X,Y))
% 14.79/14.89 | member(Z,Y) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(intersection3,axiom,
% 14.79/14.89 ( ~ member(Z,X)
% 14.79/14.89 | ~ member(Z,Y)
% 14.79/14.89 | member(Z,intersection(X,Y)) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-3: complement.
% 14.79/14.89 %----a:z:a:x:((z e ~(x)) <=> (z e universal_class) & -(z e x)).
% 14.79/14.89 cnf(complement1,axiom,
% 14.79/14.89 ( ~ member(Z,complement(X))
% 14.79/14.89 | ~ member(Z,X) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(complement2,axiom,
% 14.79/14.89 ( ~ member(Z,universal_class)
% 14.79/14.89 | member(Z,complement(X))
% 14.79/14.89 | member(Z,X) ) ).
% 14.79/14.89
% 14.79/14.89 %---- Theorem (SP2) introduces the null class O.
% 14.79/14.89
% 14.79/14.89 %----Definition of + (union).
% 14.79/14.89 %----a:x:a:y:((x + y) = ~((~(x) * ~(y)))).
% 14.79/14.89 cnf(union,axiom,
% 14.79/14.89 equalish(complement(intersection(complement(X),complement(Y))),union(X,Y)) ).
% 14.79/14.89
% 14.79/14.89 %----Definition of & (exclusive or). (= symmetric_difference).
% 14.79/14.89 %----a:x:a:y:((x y) = (~(x * y) * ~(~(x) * ~(y)))).
% 14.79/14.89 cnf(symmetric_difference,axiom,
% 14.79/14.89 equalish(intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))),symmetric_difference(X,Y)) ).
% 14.79/14.89
% 14.79/14.89 %----Definition of restriction.
% 14.79/14.89 %----a:x(restrict(xr,x,y) = (xr * cross_product(x,y))).
% 14.79/14.89 %----This is extra to the paper
% 14.79/14.89 cnf(restriction1,axiom,
% 14.79/14.89 equalish(intersection(Xr,cross_product(X,Y)),restrict(Xr,X,Y)) ).
% 14.79/14.89
% 14.79/14.89 cnf(restriction2,axiom,
% 14.79/14.89 equalish(intersection(cross_product(X,Y),Xr),restrict(Xr,X,Y)) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-4: D (domain_of).
% 14.79/14.89 %----a:y:a:z:((z e domain_of(x)) <=> (z e universal_class) &
% 14.79/14.89 %---- -(restrict(x,{z},universal_class) = O)).
% 14.79/14.89 %----next is subsumed by A-2.
% 14.79/14.89 %------> (domain_of(x) < universal_class).
% 14.79/14.89 cnf(domain1,axiom,
% 14.79/14.89 ( ~ equalish(restrict(X,singleton(Z),universal_class),null_class)
% 14.79/14.89 | ~ member(Z,domain_of(X)) ) ).
% 14.79/14.89
% 14.79/14.89 cnf(domain2,axiom,
% 14.79/14.89 ( ~ member(Z,universal_class)
% 14.79/14.89 | equalish(restrict(X,singleton(Z),universal_class),null_class)
% 14.79/14.89 | member(Z,domain_of(X)) ) ).
% 14.79/14.89
% 14.79/14.89 %----Axiom B-7: rotate.
% 14.79/14.89 %----a:x:(rotate(x) < cross_product(cross_product(universal_class,
% 14.79/14.89 %----universal_class),universal_class)).
% 14.79/14.89 %----a:x:a:u:a:v:a:w:(([[u,v],w] e rotate(x)) <=> ([[u,v],w]]
% 14.79/14.89 %---- e cross_product(cross_product(universal_class,universal_class),
% 14.79/14.89 %----universal_class)) & ([[v,w],u]] e x).
% 14.79/14.89 cnf(rotate1,axiom,
% 14.79/14.89 subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)) ).
% 14.79/14.89
% 14.79/14.90 cnf(rotate2,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X))
% 14.79/14.90 | member(ordered_pair(ordered_pair(V,W),U),X) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(rotate3,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(ordered_pair(V,W),U),X)
% 14.79/14.90 | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
% 14.79/14.90 | member(ordered_pair(ordered_pair(U,V),W),rotate(X)) ) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom B-8: flip.
% 14.79/14.90 %----a:x:(flip(x) < cross_product(cross_product(universal_class,
% 14.79/14.90 %----universal_class),universal_class)).
% 14.79/14.90 %----a:z:a:u:a:v:a:w:(([[u,v],w] e flip(x)) <=> ([[u,v],w]
% 14.79/14.90 %----e cross_product(cross_product(universal_class,universal_class),
% 14.79/14.90 %----universal_class)) & ([[v,u],w] e x).
% 14.79/14.90 cnf(flip1,axiom,
% 14.79/14.90 subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)) ).
% 14.79/14.90
% 14.79/14.90 cnf(flip2,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(ordered_pair(U,V),W),flip(X))
% 14.79/14.90 | member(ordered_pair(ordered_pair(V,U),W),X) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(flip3,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(ordered_pair(V,U),W),X)
% 14.79/14.90 | ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
% 14.79/14.90 | member(ordered_pair(ordered_pair(U,V),W),flip(X)) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of inverse.
% 14.79/14.90 %----a:y:(inverse(y) = domain_of(flip(cross_product(y,V)))).
% 14.79/14.90 cnf(inverse,axiom,
% 14.79/14.90 equalish(domain_of(flip(cross_product(Y,universal_class))),inverse(Y)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of R (range_of).
% 14.79/14.90 %----a:z:(range_of(z) = domain_of(inverse(z))).
% 14.79/14.90 cnf(range_of,axiom,
% 14.79/14.90 equalish(domain_of(inverse(Z)),range_of(Z)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of domain.
% 14.79/14.90 %----a:z:a:x:a:y:(domain(z,x,y) = first(notsub(restrict(z,x,{y}),O))).
% 14.79/14.90 cnf(domain,axiom,
% 14.79/14.90 equalish(first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)),domain(Z,X,Y)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of range.
% 14.79/14.90 %----a:z:a:x:(range(z,x,y) = second(notsub(restrict(z,{x},y),O))).
% 14.79/14.90 cnf(range,axiom,
% 14.79/14.90 equalish(second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)),range(Z,X,Y)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of image.
% 14.79/14.90 %----a:x:a:xr:((xr image x) = range_of(restrict(xr,x,V))).
% 14.79/14.90 cnf(image,axiom,
% 14.79/14.90 equalish(range_of(restrict(Xr,X,universal_class)),image(Xr,X)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of successor.
% 14.79/14.90 %----a:x:(successor(x) = (x + {x})).
% 14.79/14.90 cnf(successor,axiom,
% 14.79/14.90 equalish(union(X,singleton(X)),successor(X)) ).
% 14.79/14.90
% 14.79/14.90 %----Explicit definition of successor_relation.
% 14.79/14.90 %------> ((cross_product(V,V) * ~(((E ^ ~(inverse((E + I)))) +
% 14.79/14.90 %----(~(E) ^ inverse((E + I)))))) = successor_relation).
% 14.79/14.90 %----Definition of successor_relation from the Class Existence Theorem.
% 14.79/14.90 %----a:x:a:y:([x,y] e successor_relation <=> x e V & successor(x) = y).
% 14.79/14.90 %----The above FOF does not agree with the book
% 14.79/14.90 cnf(successor_relation1,axiom,
% 14.79/14.90 subclass(successor_relation,cross_product(universal_class,universal_class)) ).
% 14.79/14.90
% 14.79/14.90 cnf(successor_relation2,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(X,Y),successor_relation)
% 14.79/14.90 | equalish(successor(X),Y) ) ).
% 14.79/14.90
% 14.79/14.90 %----This is what's in the book and paper. Does not change axiom.
% 14.79/14.90 % input_clause(successor_relation3,axiom,
% 14.79/14.90 % [--equalish(successor(X),Y),
% 14.79/14.90 % --member(X,universal_class),
% 14.79/14.90 % ++member(ordered_pair(X,Y),successor_relation)]).
% 14.79/14.90
% 14.79/14.90 %----This is what I got by email from Quaife
% 14.79/14.90 cnf(successor_relation3,axiom,
% 14.79/14.90 ( ~ equalish(successor(X),Y)
% 14.79/14.90 | ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
% 14.79/14.90 | member(ordered_pair(X,Y),successor_relation) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of inductive a:x:(inductive(x) <=> null_class
% 14.79/14.90 %----e x & (successor_relation image x) < x)).
% 14.79/14.90 cnf(inductive1,axiom,
% 14.79/14.90 ( ~ inductive(X)
% 14.79/14.90 | member(null_class,X) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(inductive2,axiom,
% 14.79/14.90 ( ~ inductive(X)
% 14.79/14.90 | subclass(image(successor_relation,X),X) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(inductive3,axiom,
% 14.79/14.90 ( ~ member(null_class,X)
% 14.79/14.90 | ~ subclass(image(successor_relation,X),X)
% 14.79/14.90 | inductive(X) ) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom C-1: infinity.
% 14.79/14.90 %----e:x:((x e V) & inductive(x) & a:y:(inductive(y) ==> (x < y))).
% 14.79/14.90 %----e:x:((x e V) & (O e x) & ((successor_relation image x) < x)
% 14.79/14.90 %---- & a:y:((O e y) & ((successor_relation image y) < y) ==>
% 14.79/14.90 %----(x < y))).
% 14.79/14.90 cnf(omega_is_inductive1,axiom,
% 14.79/14.90 inductive(omega) ).
% 14.79/14.90
% 14.79/14.90 cnf(omega_is_inductive2,axiom,
% 14.79/14.90 ( ~ inductive(Y)
% 14.79/14.90 | subclass(omega,Y) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(omega_in_universal,axiom,
% 14.79/14.90 member(omega,universal_class) ).
% 14.79/14.90
% 14.79/14.90 %----These were commented out in the set Quaife sent me, and are not
% 14.79/14.90 %----in the paper true --> (null_class e omega).
% 14.79/14.90 %----true --> ((successor_relation image omega) < omega).
% 14.79/14.90 %----(null_class e y), ((successor_relation image y) < y) -->
% 14.79/14.90 %----(omega < y). true --> (omega e universal_class).
% 14.79/14.90
% 14.79/14.90 %----Definition of U (sum class).
% 14.79/14.90 %----a:x:(sum_class(x) = domain_of(restrict(E,V,x))).
% 14.79/14.90 cnf(sum_class_definition,axiom,
% 14.79/14.90 equalish(domain_of(restrict(element_relation,universal_class,X)),sum_class(X)) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom C-2: U (sum class).
% 14.79/14.90 %----a:x:((x e V) ==> (sum_class(x) e V)).
% 14.79/14.90 cnf(sum_class2,axiom,
% 14.79/14.90 ( ~ member(X,universal_class)
% 14.79/14.90 | member(sum_class(X),universal_class) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of P (power class).
% 14.79/14.90 %----a:x:(power_class(x) = ~((E image ~(x)))).
% 14.79/14.90 cnf(power_class_definition,axiom,
% 14.79/14.90 equalish(complement(image(element_relation,complement(X))),power_class(X)) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom C-3: P (power class).
% 14.79/14.90 %----a:u:((u e V) ==> (power_class(u) e V)).
% 14.79/14.90 cnf(power_class2,axiom,
% 14.79/14.90 ( ~ member(U,universal_class)
% 14.79/14.90 | member(power_class(U),universal_class) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of compose.
% 14.79/14.90 %----a:xr:a:yr:((yr ^ xr) < cross_product(V,V)).
% 14.79/14.90 %----a:u:a:v:a:xr:a:yr:(([u,v] e (yr ^ xr)) <=> ([u,v]
% 14.79/14.90 %----e cross_product(V,V)) & (v e (yr image (xr image {u})))).
% 14.79/14.90 cnf(compose1,axiom,
% 14.79/14.90 subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)) ).
% 14.79/14.90
% 14.79/14.90 cnf(compose2,axiom,
% 14.79/14.90 ( ~ member(ordered_pair(Y,Z),compose(Yr,Xr))
% 14.79/14.90 | member(Z,image(Yr,image(Xr,singleton(Y)))) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(compose3,axiom,
% 14.79/14.90 ( ~ member(Z,image(Yr,image(Xr,singleton(Y))))
% 14.79/14.90 | ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
% 14.79/14.90 | member(ordered_pair(Y,Z),compose(Yr,Xr)) ) ).
% 14.79/14.90
% 14.79/14.90 %----7/21/90 eliminate SINGVAL and just use FUNCTION.
% 14.79/14.90 %----Not eliminated in TPTP - I'm following the paper
% 14.79/14.90 cnf(single_valued_class1,axiom,
% 14.79/14.90 ( ~ single_valued_class(X)
% 14.79/14.90 | subclass(compose(X,inverse(X)),identity_relation) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(single_valued_class2,axiom,
% 14.79/14.90 ( ~ subclass(compose(X,inverse(X)),identity_relation)
% 14.79/14.90 | single_valued_class(X) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of function.
% 14.79/14.90 %----a:xf:(function(xf) <=> (xf < cross_product(V,V)) & ((xf
% 14.79/14.90 %----^ inverse(xf)) < identity_relation)).
% 14.79/14.90 cnf(function1,axiom,
% 14.79/14.90 ( ~ function(Xf)
% 14.79/14.90 | subclass(Xf,cross_product(universal_class,universal_class)) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(function2,axiom,
% 14.79/14.90 ( ~ function(Xf)
% 14.79/14.90 | subclass(compose(Xf,inverse(Xf)),identity_relation) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(function3,axiom,
% 14.79/14.90 ( ~ subclass(Xf,cross_product(universal_class,universal_class))
% 14.79/14.90 | ~ subclass(compose(Xf,inverse(Xf)),identity_relation)
% 14.79/14.90 | function(Xf) ) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom C-4: replacement.
% 14.79/14.90 %----a:x:((x e V) & function(xf) ==> ((xf image x) e V)).
% 14.79/14.90 cnf(replacement,axiom,
% 14.79/14.90 ( ~ function(Xf)
% 14.79/14.90 | ~ member(X,universal_class)
% 14.79/14.90 | member(image(Xf,X),universal_class) ) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom D: regularity.
% 14.79/14.90 %----a:x:(-(x = O) ==> e:u:((u e V) & (u e x) & ((u * x) = O))).
% 14.79/14.90 cnf(regularity1,axiom,
% 14.79/14.90 ( equalish(X,null_class)
% 14.79/14.90 | member(regular(X),X) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(regularity2,axiom,
% 14.79/14.90 ( equalish(X,null_class)
% 14.79/14.90 | equalish(intersection(X,regular(X)),null_class) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of apply (apply).
% 14.79/14.90 %----a:xf:a:y:((xf apply y) = sum_class((xf image {y}))).
% 14.79/14.90 cnf(apply,axiom,
% 14.79/14.90 equalish(sum_class(image(Xf,singleton(Y))),apply(Xf,Y)) ).
% 14.79/14.90
% 14.79/14.90 %----Axiom E: universal choice.
% 14.79/14.90 %----e:xf:(function(xf) & a:y:((y e V) ==> (y = null_class) |
% 14.79/14.90 %----((xf apply y) e y))).
% 14.79/14.90 cnf(choice1,axiom,
% 14.79/14.90 function(choice) ).
% 14.79/14.90
% 14.79/14.90 cnf(choice2,axiom,
% 14.79/14.90 ( ~ member(Y,universal_class)
% 14.79/14.90 | equalish(Y,null_class)
% 14.79/14.90 | member(apply(choice,Y),Y) ) ).
% 14.79/14.90
% 14.79/14.90 %----GROUP 2: MORE SET THEORY DEFINITIONS.
% 14.79/14.90
% 14.79/14.90 %----Definition of one_to_one (one-to-one function).
% 14.79/14.90 %----a:xf:(one_to_one(xf) <=> function(xf) & function(inverse(xf))).
% 14.79/14.90 cnf(one_to_one1,axiom,
% 14.79/14.90 ( ~ one_to_one(Xf)
% 14.79/14.90 | function(Xf) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(one_to_one2,axiom,
% 14.79/14.90 ( ~ one_to_one(Xf)
% 14.79/14.90 | function(inverse(Xf)) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(one_to_one3,axiom,
% 14.79/14.90 ( ~ function(inverse(Xf))
% 14.79/14.90 | ~ function(Xf)
% 14.79/14.90 | one_to_one(Xf) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of S (subset relation).
% 14.79/14.90 cnf(subset_relation,axiom,
% 14.79/14.90 equalish(intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))),subset_relation) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of I (identity relation).
% 14.79/14.90 cnf(identity_relation,axiom,
% 14.79/14.90 equalish(intersection(inverse(subset_relation),subset_relation),identity_relation) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of diagonalization.
% 14.79/14.90 %----a:xr:(diagonalise(xr) = ~(domain_of((identity_relation * xr)))).
% 14.79/14.90 cnf(diagonalisation,axiom,
% 14.79/14.90 equalish(complement(domain_of(intersection(Xr,identity_relation))),diagonalise(Xr)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of Cantor class.
% 14.79/14.90 cnf(cantor_class,axiom,
% 14.79/14.90 equalish(intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))),cantor(X)) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of operation.
% 14.79/14.90 %----a:xf:(operation(xf) <=> function(xf) & (cross_product(domain_of(
% 14.79/14.90 %----domain_of(xf)),domain_of(domain_of(xf))) = domain_of(xf))
% 14.79/14.90 %----& (range_of(xf) < domain_of(domain_of(xf))).
% 14.79/14.90 cnf(operation1,axiom,
% 14.79/14.90 ( ~ operation(Xf)
% 14.79/14.90 | function(Xf) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(operation2,axiom,
% 14.79/14.90 ( ~ operation(Xf)
% 14.79/14.90 | equalish(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf)) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(operation3,axiom,
% 14.79/14.90 ( ~ operation(Xf)
% 14.79/14.90 | subclass(range_of(Xf),domain_of(domain_of(Xf))) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(operation4,axiom,
% 14.79/14.90 ( ~ function(Xf)
% 14.79/14.90 | ~ equalish(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))
% 14.79/14.90 | ~ subclass(range_of(Xf),domain_of(domain_of(Xf)))
% 14.79/14.90 | operation(Xf) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of compatible.
% 14.79/14.90 %----a:xh:a:xf1:a:af2: (compatible(xh,xf1,xf2) <=> function(xh)
% 14.79/14.90 %----& (domain_of(domain_of(xf1)) = domain_of(xh)) & (range_of(xh)
% 14.79/14.90 %----< domain_of(domain_of(xf2)))).
% 14.79/14.90 cnf(compatible1,axiom,
% 14.79/14.90 ( ~ compatible(Xh,Xf1,Xf2)
% 14.79/14.90 | function(Xh) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(compatible2,axiom,
% 14.79/14.90 ( ~ compatible(Xh,Xf1,Xf2)
% 14.79/14.90 | equalish(domain_of(domain_of(Xf1)),domain_of(Xh)) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(compatible3,axiom,
% 14.79/14.90 ( ~ compatible(Xh,Xf1,Xf2)
% 14.79/14.90 | subclass(range_of(Xh),domain_of(domain_of(Xf2))) ) ).
% 14.79/14.90
% 14.79/14.90 cnf(compatible4,axiom,
% 14.79/14.90 ( ~ function(Xh)
% 14.79/14.90 | ~ equalish(domain_of(domain_of(Xf1)),domain_of(Xh))
% 14.79/14.90 | ~ subclass(range_of(Xh),domain_of(domain_of(Xf2)))
% 14.79/14.90 | compatible(Xh1,Xf1,Xf2) ) ).
% 14.79/14.90
% 14.79/14.90 %----Definition of homomorphism.
% 14.79/14.90 %----a:xh:a:xf1:a:xf2: (homomorphism(xh,xf1,xf2) <=>
% 14.79/14.90 %---- operation(xf1) & operation(xf2) & compatible(xh,xf1,xf2) &
% 14.79/14.90 %---- a:x:a:y:(([x,y] e domain_of(xf1)) ==> (((xf2 apply [(xh apply x),
% 14.79/14.90 %----(xh apply y)]) = (xh apply (xf1 apply [x,y])))).
% 14.79/14.90 cnf(homomorphism1,axiom,
% 14.79/14.90 ( ~ homomorphism(Xh,Xf1,Xf2)
% 14.79/14.90 | operation(Xf1) ) ).
% 14.79/14.90
% 14.79/14.91 cnf(homomorphism2,axiom,
% 14.79/14.91 ( ~ homomorphism(Xh,Xf1,Xf2)
% 14.79/14.91 | operation(Xf2) ) ).
% 14.79/14.91
% 14.79/14.91 cnf(homomorphism3,axiom,
% 14.79/14.91 ( ~ homomorphism(Xh,Xf1,Xf2)
% 14.79/14.91 | compatible(Xh,Xf1,Xf2) ) ).
% 14.79/14.91
% 14.79/14.91 cnf(homomorphism4,axiom,
% 14.79/14.91 ( ~ homomorphism(Xh,Xf1,Xf2)
% 14.79/14.91 | ~ member(ordered_pair(X,Y),domain_of(Xf1))
% 14.79/14.91 | equalish(apply(Xf2,ordered_pair(apply(Xh,X),apply(Xh,Y))),apply(Xh,apply(Xf1,ordered_pair(X,Y)))) ) ).
% 14.79/14.91
% 14.79/14.91 cnf(homomorphism5,axiom,
% 14.79/14.91 ( ~ operation(Xf1)
% 14.79/14.91 | ~ operation(Xf2)
% 14.79/14.91 | ~ compatible(Xh,Xf1,Xf2)
% 14.79/14.91 | member(ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)),domain_of(Xf1))
% 14.79/14.91 | homomorphism(Xh,Xf1,Xf2) ) ).
% 14.79/14.91
% 14.79/14.91 cnf(homomorphism6,axiom,
% 14.79/14.91 ( ~ operation(Xf1)
% 14.79/14.91 | ~ operation(Xf2)
% 14.79/14.91 | ~ compatible(Xh,Xf1,Xf2)
% 14.79/14.91 | ~ equalish(apply(Xf2,ordered_pair(apply(Xh,not_homomorphism1(Xh,Xf1,Xf2)),apply(Xh,not_homomorphism2(Xh,Xf1,Xf2)))),apply(Xh,apply(Xf1,ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)))))
% 14.79/14.91 | homomorphism(Xh,Xf1,Xf2) ) ).
% 14.79/14.91
% 14.79/14.91 cnf(prove_reflexivity,negated_conjecture,
% 14.79/14.91 ~ equalish(x,x) ).
% 14.79/14.91
% 14.79/14.91 %--------------------------------------------------------------------------
% 14.79/14.91 %-------------------------------------------
% 14.79/14.91 % Proof found
% 14.79/14.91 % SZS status Theorem for theBenchmark
% 14.79/14.91 % SZS output start Proof
% 14.79/14.91 %ClaNum:159(EqnAxiom:0)
% 14.79/14.91 %VarNum:815(SingletonVarNum:378)
% 14.79/14.91 %MaxLitNum:5
% 14.79/14.91 %MaxfuncDepth:5
% 14.79/14.91 %SharedTerms:27
% 14.79/14.91 %goalClause: 30
% 14.79/14.91 %singleGoalClaCount:1
% 14.79/14.91 [1]P1(a1)
% 14.79/14.91 [2]P4(a4)
% 14.79/14.91 [3]P6(a4,a22)
% 14.79/14.91 [30]~P2(a39,a39)
% 14.79/14.91 [5]P7(a5,f6(a22,a22))
% 14.79/14.91 [6]P7(a23,f6(a22,a22))
% 14.79/14.91 [9]P2(f13(f12(a28),a28),a14)
% 14.79/14.91 [27]P2(f13(f6(a22,a22),f13(f6(a22,a22),f8(f7(f8(a5),f12(a5))))),a28)
% 14.79/14.91 [4]P7(x41,a22)
% 14.79/14.91 [10]P2(f38(x101,x101),f29(x101))
% 14.79/14.91 [8]P2(f9(f12(x81)),f24(x81))
% 14.79/14.91 [11]P2(f35(x111,f29(x111)),f34(x111))
% 14.79/14.91 [13]P7(f15(x131),f6(f6(a22,a22),a22))
% 14.79/14.91 [14]P7(f30(x141),f6(f6(a22,a22),a22))
% 14.79/14.91 [24]P2(f9(f31(a5,a22,x241)),f36(x241))
% 14.79/14.91 [15]P2(f8(f17(a5,f8(x151))),f25(x151))
% 14.79/14.91 [17]P2(f8(f9(f13(x171,a14))),f10(x171))
% 14.79/14.91 [18]P2(f9(f15(f6(x181,a22))),f12(x181))
% 14.79/14.91 [23]P2(f13(f9(x231),f10(f7(f12(a5),x231))),f3(x231))
% 14.79/14.91 [7]P6(f38(x71,x72),a22)
% 14.79/14.91 [12]P7(f7(x121,x122),f6(a22,a22))
% 14.79/14.91 [25]P2(f24(f31(x251,x252,a22)),f17(x251,x252))
% 14.79/14.91 [16]P2(f36(f17(x161,f29(x162))),f2(x161,x162))
% 14.79/14.91 [19]P2(f8(f13(f8(x191),f8(x192))),f35(x191,x192))
% 14.79/14.91 [20]P2(f38(f29(x201),f38(x201,f29(x202))),f26(x201,x202))
% 14.79/14.91 [26]P2(f13(f8(f13(x261,x262)),f8(f13(f8(x261),f8(x262)))),f37(x261,x262))
% 14.79/14.91 [21]P2(f13(x211,f6(x212,x213)),f31(x211,x212,x213))
% 14.79/14.91 [22]P2(f13(f6(x221,x222),x223),f31(x223,x221,x222))
% 14.79/14.91 [28]P2(f16(f19(f31(x281,x282,f29(x283)),a18)),f11(x281,x282,x283))
% 14.79/14.91 [29]P2(f33(f19(f31(x291,f29(x292),x293),a18)),f27(x291,x292,x293))
% 14.79/14.91 [31]~P8(x311)+P1(x311)
% 14.79/14.91 [32]~P9(x321)+P1(x321)
% 14.79/14.91 [34]~P4(x341)+P6(a18,x341)
% 14.79/14.91 [35]~P4(x351)+P7(a4,x351)
% 14.79/14.91 [33]~P8(x331)+P1(f12(x331))
% 14.79/14.91 [37]P6(f32(x371),x371)+P2(x371,a18)
% 14.79/14.91 [46]~P6(x461,a22)+P6(f25(x461),a22)
% 14.79/14.91 [47]~P6(x471,a22)+P6(f36(x471),a22)
% 14.79/14.91 [48]~P1(x481)+P7(x481,f6(a22,a22))
% 14.79/14.91 [49]~P4(x491)+P7(f17(a23,x491),x491)
% 14.79/14.91 [50]~P9(x501)+P7(f24(x501),f9(f9(x501)))
% 14.79/14.91 [69]~P1(x691)+P7(f7(x691,f12(x691)),a14)
% 14.79/14.91 [70]~P10(x701)+P7(f7(x701,f12(x701)),a14)
% 14.79/14.91 [80]P2(x801,a18)+P2(f13(x801,f32(x801)),a18)
% 14.79/14.91 [89]P10(x891)+~P7(f7(x891,f12(x891)),a14)
% 14.79/14.91 [120]~P9(x1201)+P2(f6(f9(f9(x1201)),f9(f9(x1201))),f9(x1201))
% 14.79/14.91 [43]~P2(x432,x431)+P2(x431,x432)
% 14.79/14.91 [44]~P2(x442,x441)+P7(x441,x442)
% 14.79/14.91 [45]~P2(x451,x452)+P7(x451,x452)
% 14.79/14.91 [51]~P2(x511,x512)+P2(f3(x511),f3(x512))
% 14.79/14.91 [52]~P2(x521,x522)+P2(f8(x521),f8(x522))
% 14.79/14.91 [53]~P2(x531,x532)+P2(f10(x531),f10(x532))
% 14.79/14.91 [54]~P2(x541,x542)+P2(f9(x541),f9(x542))
% 14.79/14.91 [55]~P2(x551,x552)+P2(f16(x551),f16(x552))
% 14.79/14.91 [56]~P2(x561,x562)+P2(f15(x561),f15(x562))
% 14.79/14.91 [57]~P2(x571,x572)+P2(f12(x571),f12(x572))
% 14.79/14.91 [58]~P2(x581,x582)+P2(f25(x581),f25(x582))
% 14.79/14.91 [59]~P2(x591,x592)+P2(f24(x591),f24(x592))
% 14.79/14.91 [60]~P2(x601,x602)+P2(f32(x601),f32(x602))
% 14.79/14.91 [61]~P2(x611,x612)+P2(f30(x611),f30(x612))
% 14.79/14.91 [62]~P2(x621,x622)+P2(f33(x621),f33(x622))
% 14.79/14.91 [63]~P2(x631,x632)+P2(f29(x631),f29(x632))
% 14.79/14.91 [64]~P2(x641,x642)+P2(f34(x641),f34(x642))
% 14.79/14.91 [65]~P2(x651,x652)+P2(f36(x651),f36(x652))
% 14.79/14.91 [66]P7(x661,x662)+P6(f19(x661,x662),x661)
% 14.79/14.91 [67]~P6(x671,x672)+~P6(x671,f8(x672))
% 14.79/14.91 [78]~P6(x781,a22)+P6(x781,f38(x782,x781))
% 14.79/14.91 [79]~P6(x791,a22)+P6(x791,f38(x791,x792))
% 14.79/14.91 [83]P6(x831,x832)+~P6(f26(x831,x832),a5)
% 14.79/14.91 [86]P7(x861,x862)+~P6(f19(x861,x862),x862)
% 14.79/14.91 [87]P2(f34(x871),x872)+~P6(f26(x871,x872),a23)
% 14.79/14.91 [135]~P6(x1351,f9(x1352))+~P2(f31(x1352,f29(x1351),a22),a18)
% 14.79/14.91 [111]P1(x1111)+~P3(x1111,x1112,x1113)
% 14.79/14.91 [112]P9(x1121)+~P5(x1122,x1123,x1121)
% 14.79/14.91 [113]P9(x1131)+~P5(x1132,x1131,x1133)
% 14.79/14.91 [123]~P5(x1231,x1232,x1233)+P3(x1231,x1232,x1233)
% 14.79/14.91 [84]P6(x841,x842)+~P6(x841,f13(x843,x842))
% 14.79/14.91 [85]P6(x851,x852)+~P6(x851,f13(x852,x853))
% 14.79/14.91 [91]~P2(x912,x913)+P2(f2(x911,x912),f2(x911,x913))
% 14.79/14.91 [92]~P2(x921,x923)+P2(f2(x921,x922),f2(x923,x922))
% 14.79/14.91 [93]~P2(x932,x933)+P2(f7(x931,x932),f7(x931,x933))
% 14.79/14.91 [94]~P2(x941,x943)+P2(f7(x941,x942),f7(x943,x942))
% 14.79/14.91 [95]~P2(x952,x953)+P2(f6(x951,x952),f6(x951,x953))
% 14.79/14.91 [96]~P2(x961,x963)+P2(f6(x961,x962),f6(x963,x962))
% 14.79/14.91 [97]~P2(x972,x973)+P2(f37(x971,x972),f37(x971,x973))
% 14.79/14.91 [98]~P2(x981,x983)+P2(f37(x981,x982),f37(x983,x982))
% 14.79/14.91 [99]~P2(x992,x993)+P2(f17(x991,x992),f17(x991,x993))
% 14.79/14.91 [100]~P2(x1001,x1003)+P2(f17(x1001,x1002),f17(x1003,x1002))
% 14.79/14.91 [101]~P2(x1012,x1013)+P2(f13(x1011,x1012),f13(x1011,x1013))
% 14.79/14.91 [102]~P2(x1021,x1023)+P2(f13(x1021,x1022),f13(x1023,x1022))
% 14.79/14.91 [103]~P2(x1032,x1033)+P2(f19(x1031,x1032),f19(x1031,x1033))
% 14.79/14.91 [104]~P2(x1041,x1043)+P2(f19(x1041,x1042),f19(x1043,x1042))
% 14.79/14.91 [105]~P2(x1052,x1053)+P2(f26(x1051,x1052),f26(x1051,x1053))
% 14.79/14.91 [106]~P2(x1061,x1063)+P2(f26(x1061,x1062),f26(x1063,x1062))
% 14.79/14.91 [107]~P2(x1072,x1073)+P2(f35(x1071,x1072),f35(x1071,x1073))
% 14.79/14.91 [108]~P2(x1081,x1083)+P2(f35(x1081,x1082),f35(x1083,x1082))
% 14.79/14.91 [109]~P2(x1092,x1093)+P2(f38(x1091,x1092),f38(x1091,x1093))
% 14.79/14.91 [110]~P2(x1101,x1103)+P2(f38(x1101,x1102),f38(x1103,x1102))
% 14.79/14.91 [118]~P3(x1181,x1183,x1182)+P7(f24(x1181),f9(f9(x1182)))
% 14.79/14.91 [119]~P3(x1192,x1191,x1193)+P2(f9(f9(x1191)),f9(x1192))
% 14.79/14.91 [121]~P6(x1211,f6(x1212,x1213))+P2(f26(f16(x1211),f33(x1211)),x1211)
% 14.79/14.91 [116]P6(x1161,x1162)+~P6(f26(x1163,x1161),f6(x1164,x1162))
% 14.79/14.91 [117]P6(x1171,x1172)+~P6(f26(x1171,x1173),f6(x1172,x1174))
% 14.79/14.91 [138]~P2(x1383,x1384)+P2(f11(x1381,x1382,x1383),f11(x1381,x1382,x1384))
% 14.79/14.91 [139]~P2(x1392,x1394)+P2(f11(x1391,x1392,x1393),f11(x1391,x1394,x1393))
% 14.79/14.91 [140]~P2(x1401,x1404)+P2(f11(x1401,x1402,x1403),f11(x1404,x1402,x1403))
% 14.79/14.91 [141]~P2(x1413,x1414)+P2(f20(x1411,x1412,x1413),f20(x1411,x1412,x1414))
% 14.79/14.91 [142]~P2(x1422,x1424)+P2(f20(x1421,x1422,x1423),f20(x1421,x1424,x1423))
% 14.79/14.91 [143]~P2(x1431,x1434)+P2(f20(x1431,x1432,x1433),f20(x1434,x1432,x1433))
% 14.79/14.91 [144]~P2(x1443,x1444)+P2(f21(x1441,x1442,x1443),f21(x1441,x1442,x1444))
% 14.79/14.91 [145]~P2(x1452,x1454)+P2(f21(x1451,x1452,x1453),f21(x1451,x1454,x1453))
% 14.79/14.91 [146]~P2(x1461,x1464)+P2(f21(x1461,x1462,x1463),f21(x1464,x1462,x1463))
% 14.79/14.91 [147]~P2(x1473,x1474)+P2(f27(x1471,x1472,x1473),f27(x1471,x1472,x1474))
% 14.79/14.91 [148]~P2(x1482,x1484)+P2(f27(x1481,x1482,x1483),f27(x1481,x1484,x1483))
% 14.79/14.91 [149]~P2(x1491,x1494)+P2(f27(x1491,x1492,x1493),f27(x1494,x1492,x1493))
% 14.79/14.91 [150]~P2(x1503,x1504)+P2(f31(x1501,x1502,x1503),f31(x1501,x1502,x1504))
% 14.79/14.91 [151]~P2(x1512,x1514)+P2(f31(x1511,x1512,x1513),f31(x1511,x1514,x1513))
% 14.79/14.91 [152]~P2(x1521,x1524)+P2(f31(x1521,x1522,x1523),f31(x1524,x1522,x1523))
% 14.79/14.91 [136]~P6(f26(f26(x1363,x1361),x1362),f30(x1364))+P6(f26(f26(x1361,x1362),x1363),x1364)
% 14.79/14.91 [137]~P6(f26(f26(x1372,x1371),x1373),f15(x1374))+P6(f26(f26(x1371,x1372),x1373),x1374)
% 14.79/14.91 [134]~P6(f26(x1344,x1341),f7(x1342,x1343))+P6(x1341,f17(x1342,f17(x1343,f29(x1344))))
% 14.79/14.91 [36]~P1(x361)+P8(x361)+~P1(f12(x361))
% 14.79/14.91 [82]~P6(x821,a22)+P2(x821,a18)+P6(f2(a1,x821),x821)
% 14.79/14.91 [88]P4(x881)+~P6(a18,x881)+~P7(f17(a23,x881),x881)
% 14.79/14.91 [122]P1(x1221)+~P7(x1221,f6(a22,a22))+~P7(f7(x1221,f12(x1221)),a14)
% 14.79/14.91 [38]~P2(x382,x381)+P1(x381)+~P1(x382)
% 14.79/14.91 [39]~P2(x392,x391)+P4(x391)+~P4(x392)
% 14.79/14.91 [40]~P2(x402,x401)+P8(x401)+~P8(x402)
% 14.79/14.91 [41]~P2(x412,x411)+P9(x411)+~P9(x412)
% 14.79/14.91 [42]~P2(x422,x421)+P10(x421)+~P10(x422)
% 14.79/14.91 [72]~P7(x722,x721)+~P7(x721,x722)+P2(x721,x722)
% 14.79/14.91 [68]P6(x681,x682)+P6(x681,f8(x682))+~P6(x681,a22)
% 14.79/14.91 [81]~P1(x811)+~P6(x812,a22)+P6(f17(x811,x812),a22)
% 14.79/14.91 [124]~P6(x1241,x1242)+~P6(f26(x1241,x1242),f6(a22,a22))+P6(f26(x1241,x1242),a5)
% 14.79/14.91 [131]~P2(f34(x1311),x1312)+~P6(f26(x1311,x1312),f6(a22,a22))+P6(f26(x1311,x1312),a23)
% 14.79/14.91 [132]~P6(x1321,a22)+P6(x1321,f9(x1322))+P2(f31(x1322,f29(x1321),a22),a18)
% 14.79/14.91 [71]~P2(x711,x713)+P2(x711,x712)+~P2(x713,x712)
% 14.79/14.91 [73]~P6(x731,x733)+P6(x731,x732)+~P2(x733,x732)
% 14.79/14.91 [74]~P7(x743,x742)+P6(x741,x742)+~P6(x741,x743)
% 14.79/14.91 [75]~P6(x753,x752)+P6(x751,x752)+~P2(x753,x751)
% 14.79/14.91 [76]~P7(x761,x763)+P7(x761,x762)+~P2(x763,x762)
% 14.79/14.91 [77]~P7(x773,x772)+P7(x771,x772)+~P2(x773,x771)
% 14.79/14.91 [90]~P6(x901,x903)+~P6(x901,x902)+P6(x901,f13(x902,x903))
% 14.79/14.91 [114]P2(x1141,x1142)+P2(x1141,x1143)+~P6(x1141,f38(x1143,x1142))
% 14.79/14.91 [125]~P3(x1251,x1252,x1254)+P3(x1251,x1252,x1253)+~P2(x1254,x1253)
% 14.79/14.91 [126]~P3(x1261,x1264,x1263)+P3(x1261,x1262,x1263)+~P2(x1264,x1262)
% 14.79/14.91 [127]~P3(x1274,x1272,x1273)+P3(x1271,x1272,x1273)+~P2(x1274,x1271)
% 14.79/14.91 [128]~P5(x1281,x1282,x1284)+P5(x1281,x1282,x1283)+~P2(x1284,x1283)
% 14.79/14.91 [129]~P5(x1291,x1294,x1293)+P5(x1291,x1292,x1293)+~P2(x1294,x1292)
% 14.79/14.91 [130]~P5(x1304,x1302,x1303)+P5(x1301,x1302,x1303)+~P2(x1304,x1301)
% 14.79/14.91 [115]~P6(x1152,x1154)+~P6(x1151,x1153)+P6(f26(x1151,x1152),f6(x1153,x1154))
% 14.79/14.91 [155]~P6(f26(f26(x1552,x1553),x1551),x1554)+P6(f26(f26(x1551,x1552),x1553),f30(x1554))+~P6(f26(f26(x1551,x1552),x1553),f6(f6(a22,a22),a22))
% 14.79/14.91 [156]~P6(f26(f26(x1562,x1561),x1563),x1564)+P6(f26(f26(x1561,x1562),x1563),f15(x1564))+~P6(f26(f26(x1561,x1562),x1563),f6(f6(a22,a22),a22))
% 14.79/14.91 [154]P6(f26(x1541,x1542),f7(x1543,x1544))+~P6(f26(x1541,x1542),f6(a22,a22))+~P6(x1542,f17(x1543,f17(x1544,f29(x1541))))
% 14.79/14.91 [158]~P5(x1582,x1585,x1581)+~P6(f26(x1583,x1584),f9(x1585))+P2(f2(x1581,f26(f2(x1582,x1583),f2(x1582,x1584))),f2(x1582,f2(x1585,f26(x1583,x1584))))
% 14.79/14.91 [153]~P1(x1531)+P9(x1531)+~P7(f24(x1531),f9(f9(x1531)))+~P2(f6(f9(f9(x1531)),f9(f9(x1531))),f9(x1531))
% 14.79/14.91 [133]P3(x1331,x1332,x1333)+~P1(x1334)+~P7(f24(x1334),f9(f9(x1333)))+~P2(f9(f9(x1332)),f9(x1334))
% 14.79/14.91 [157]~P9(x1573)+~P9(x1572)+~P3(x1571,x1572,x1573)+P5(x1571,x1572,x1573)+P6(f26(f20(x1571,x1572,x1573),f21(x1571,x1572,x1573)),f9(x1572))
% 14.79/14.91 [159]~P9(x1593)+~P9(x1592)+~P3(x1591,x1592,x1593)+P5(x1591,x1592,x1593)+~P2(f2(x1593,f26(f2(x1591,f20(x1591,x1592,x1593)),f2(x1591,f21(x1591,x1592,x1593)))),f2(x1591,f2(x1592,f26(f20(x1591,x1592,x1593),f21(x1591,x1592,x1593)))))
% 14.79/14.91 %EqnAxiom
% 14.79/14.91
% 14.79/14.91 %-------------------------------------------
% 14.79/14.91 cnf(4199,plain,
% 14.79/14.91 (P6(f19(a39,a39),a39)),
% 14.79/14.91 inference(scs_inference,[],[30,66,72])).
% 14.79/14.91 cnf(4205,plain,
% 14.79/14.91 ($false),
% 14.79/14.91 inference(scs_inference,[],[30,4,4199,86,74,72]),
% 14.79/14.91 ['proof']).
% 14.79/14.91 % SZS output end Proof
% 14.79/14.91 % Total time :14.240000s
%------------------------------------------------------------------------------