%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT379+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 13:12:43 EST 2010
% Result : Theorem 1.78s
% Output : Solution 1.78s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP24563/LAT379+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP24563/LAT379+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP24563/LAT379+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 24659
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.023 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v5_waybel34(X3,X1,X2)<=>r4_waybel_0(X1,X2,X3,k1_pre_topc(X1)))))),file('/tmp/SRASS.s.p', d16_waybel34)).
% fof(4, axiom,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v20_waybel_0(X3,X1,X2)<=>![X4]:(m1_subset_1(X4,u1_struct_0(X1))=>![X5]:(m1_subset_1(X5,u1_struct_0(X1))=>r4_waybel_0(X1,X2,X3,k2_struct_0(X1,X4,X5)))))))),file('/tmp/SRASS.s.p', d35_waybel_0)).
% fof(5, axiom,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v4_waybel34(X3,X1,X2)<=>![X4]:((v1_finset_1(X4)&m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1))))=>r4_waybel_0(X1,X2,X3,X4)))))),file('/tmp/SRASS.s.p', d15_waybel34)).
% fof(9, axiom,![X1]:(l1_orders_2(X1)=>l1_struct_0(X1)),file('/tmp/SRASS.s.p', dt_l1_orders_2)).
% fof(21, axiom,![X1]:![X2]:![X3]:((((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))&m1_subset_1(X3,u1_struct_0(X1)))=>m1_subset_1(k2_struct_0(X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_k2_struct_0)).
% fof(34, axiom,![X1]:(v1_xboole_0(X1)=>v1_finset_1(X1)),file('/tmp/SRASS.s.p', cc1_finset_1)).
% fof(35, axiom,![X1]:(l1_struct_0(X1)=>m1_subset_1(k1_pre_topc(X1),k1_zfmisc_1(u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_k1_pre_topc)).
% fof(37, axiom,![X1]:![X2]:![X3]:((((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))&m1_subset_1(X3,u1_struct_0(X1)))=>k2_struct_0(X1,X2,X3)=k2_tarski(X2,X3)),file('/tmp/SRASS.s.p', redefinition_k2_struct_0)).
% fof(46, axiom,![X1]:![X2]:(~(v1_xboole_0(k2_tarski(X1,X2)))&v1_finset_1(k2_tarski(X1,X2))),file('/tmp/SRASS.s.p', fc2_finset_1)).
% fof(70, axiom,![X1]:(l1_struct_0(X1)=>(((((v1_xboole_0(k1_pre_topc(X1))&v1_membered(k1_pre_topc(X1)))&v2_membered(k1_pre_topc(X1)))&v3_membered(k1_pre_topc(X1)))&v4_membered(k1_pre_topc(X1)))&v5_membered(k1_pre_topc(X1)))),file('/tmp/SRASS.s.p', fc1_pre_topc)).
% fof(83, conjecture,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v4_waybel34(X3,X1,X2)=>(v20_waybel_0(X3,X1,X2)&v5_waybel34(X3,X1,X2)))))),file('/tmp/SRASS.s.p', t65_waybel34)).
% fof(84, negated_conjecture,~(![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v4_waybel34(X3,X1,X2)=>(v20_waybel_0(X3,X1,X2)&v5_waybel34(X3,X1,X2))))))),inference(assume_negation,[status(cth)],[83])).
% fof(85, plain,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v5_waybel34(X3,X1,X2)<=>r4_waybel_0(X1,X2,X3,k1_pre_topc(X1)))))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(86, plain,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v20_waybel_0(X3,X1,X2)<=>![X4]:(m1_subset_1(X4,u1_struct_0(X1))=>![X5]:(m1_subset_1(X5,u1_struct_0(X1))=>r4_waybel_0(X1,X2,X3,k2_struct_0(X1,X4,X5)))))))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(87, plain,![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v4_waybel34(X3,X1,X2)<=>![X4]:((v1_finset_1(X4)&m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1))))=>r4_waybel_0(X1,X2,X3,X4)))))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(93, plain,![X1]:![X2]:![X3]:((((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))&m1_subset_1(X3,u1_struct_0(X1)))=>m1_subset_1(k2_struct_0(X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[21,theory(equality)])).
% fof(98, plain,![X1]:![X2]:![X3]:((((~(v3_struct_0(X1))&l1_struct_0(X1))&m1_subset_1(X2,u1_struct_0(X1)))&m1_subset_1(X3,u1_struct_0(X1)))=>k2_struct_0(X1,X2,X3)=k2_tarski(X2,X3)),inference(fof_simplification,[status(thm)],[37,theory(equality)])).
% fof(99, plain,![X1]:![X2]:(~(v1_xboole_0(k2_tarski(X1,X2)))&v1_finset_1(k2_tarski(X1,X2))),inference(fof_simplification,[status(thm)],[46,theory(equality)])).
% fof(104, negated_conjecture,~(![X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))=>![X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))=>(v4_waybel34(X3,X1,X2)=>(v20_waybel_0(X3,X1,X2)&v5_waybel34(X3,X1,X2))))))),inference(fof_simplification,[status(thm)],[84,theory(equality)])).
% fof(111, plain,![X1]:((v3_struct_0(X1)|~(l1_orders_2(X1)))|![X2]:((v3_struct_0(X2)|~(l1_orders_2(X2)))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((~(v5_waybel34(X3,X1,X2))|r4_waybel_0(X1,X2,X3,k1_pre_topc(X1)))&(~(r4_waybel_0(X1,X2,X3,k1_pre_topc(X1)))|v5_waybel34(X3,X1,X2)))))),inference(fof_nnf,[status(thm)],[85])).
% fof(112, plain,![X4]:((v3_struct_0(X4)|~(l1_orders_2(X4)))|![X5]:((v3_struct_0(X5)|~(l1_orders_2(X5)))|![X6]:(((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((~(v5_waybel34(X6,X4,X5))|r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))&(~(r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))|v5_waybel34(X6,X4,X5)))))),inference(variable_rename,[status(thm)],[111])).
% fof(113, plain,![X4]:![X5]:![X6]:(((((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5))))|((~(v5_waybel34(X6,X4,X5))|r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))&(~(r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))|v5_waybel34(X6,X4,X5))))|(v3_struct_0(X5)|~(l1_orders_2(X5))))|(v3_struct_0(X4)|~(l1_orders_2(X4)))),inference(shift_quantors,[status(thm)],[112])).
% fof(114, plain,![X4]:![X5]:![X6]:(((((~(v5_waybel34(X6,X4,X5))|r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))|((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))|(v3_struct_0(X5)|~(l1_orders_2(X5))))|(v3_struct_0(X4)|~(l1_orders_2(X4))))&((((~(r4_waybel_0(X4,X5,X6,k1_pre_topc(X4)))|v5_waybel34(X6,X4,X5))|((~(v1_funct_1(X6))|~(v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5))))|~(m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))))|(v3_struct_0(X5)|~(l1_orders_2(X5))))|(v3_struct_0(X4)|~(l1_orders_2(X4))))),inference(distribute,[status(thm)],[113])).
% cnf(115,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v5_waybel34(X3,X1,X2)|~l1_orders_2(X1)|~l1_orders_2(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)|~r4_waybel_0(X1,X2,X3,k1_pre_topc(X1))),inference(split_conjunct,[status(thm)],[114])).
% fof(117, plain,![X1]:((v3_struct_0(X1)|~(l1_orders_2(X1)))|![X2]:((v3_struct_0(X2)|~(l1_orders_2(X2)))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((~(v20_waybel_0(X3,X1,X2))|![X4]:(~(m1_subset_1(X4,u1_struct_0(X1)))|![X5]:(~(m1_subset_1(X5,u1_struct_0(X1)))|r4_waybel_0(X1,X2,X3,k2_struct_0(X1,X4,X5)))))&(?[X4]:(m1_subset_1(X4,u1_struct_0(X1))&?[X5]:(m1_subset_1(X5,u1_struct_0(X1))&~(r4_waybel_0(X1,X2,X3,k2_struct_0(X1,X4,X5)))))|v20_waybel_0(X3,X1,X2)))))),inference(fof_nnf,[status(thm)],[86])).
% fof(118, plain,![X6]:((v3_struct_0(X6)|~(l1_orders_2(X6)))|![X7]:((v3_struct_0(X7)|~(l1_orders_2(X7)))|![X8]:(((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7))))|((~(v20_waybel_0(X8,X6,X7))|![X9]:(~(m1_subset_1(X9,u1_struct_0(X6)))|![X10]:(~(m1_subset_1(X10,u1_struct_0(X6)))|r4_waybel_0(X6,X7,X8,k2_struct_0(X6,X9,X10)))))&(?[X11]:(m1_subset_1(X11,u1_struct_0(X6))&?[X12]:(m1_subset_1(X12,u1_struct_0(X6))&~(r4_waybel_0(X6,X7,X8,k2_struct_0(X6,X11,X12)))))|v20_waybel_0(X8,X6,X7)))))),inference(variable_rename,[status(thm)],[117])).
% fof(119, plain,![X6]:((v3_struct_0(X6)|~(l1_orders_2(X6)))|![X7]:((v3_struct_0(X7)|~(l1_orders_2(X7)))|![X8]:(((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7))))|((~(v20_waybel_0(X8,X6,X7))|![X9]:(~(m1_subset_1(X9,u1_struct_0(X6)))|![X10]:(~(m1_subset_1(X10,u1_struct_0(X6)))|r4_waybel_0(X6,X7,X8,k2_struct_0(X6,X9,X10)))))&((m1_subset_1(esk3_3(X6,X7,X8),u1_struct_0(X6))&(m1_subset_1(esk4_3(X6,X7,X8),u1_struct_0(X6))&~(r4_waybel_0(X6,X7,X8,k2_struct_0(X6,esk3_3(X6,X7,X8),esk4_3(X6,X7,X8))))))|v20_waybel_0(X8,X6,X7)))))),inference(skolemize,[status(esa)],[118])).
% fof(120, plain,![X6]:![X7]:![X8]:![X9]:![X10]:(((((((~(m1_subset_1(X10,u1_struct_0(X6)))|r4_waybel_0(X6,X7,X8,k2_struct_0(X6,X9,X10)))|~(m1_subset_1(X9,u1_struct_0(X6))))|~(v20_waybel_0(X8,X6,X7)))&((m1_subset_1(esk3_3(X6,X7,X8),u1_struct_0(X6))&(m1_subset_1(esk4_3(X6,X7,X8),u1_struct_0(X6))&~(r4_waybel_0(X6,X7,X8,k2_struct_0(X6,esk3_3(X6,X7,X8),esk4_3(X6,X7,X8))))))|v20_waybel_0(X8,X6,X7)))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7)))))|(v3_struct_0(X7)|~(l1_orders_2(X7))))|(v3_struct_0(X6)|~(l1_orders_2(X6)))),inference(shift_quantors,[status(thm)],[119])).
% fof(121, plain,![X6]:![X7]:![X8]:![X9]:![X10]:(((((((~(m1_subset_1(X10,u1_struct_0(X6)))|r4_waybel_0(X6,X7,X8,k2_struct_0(X6,X9,X10)))|~(m1_subset_1(X9,u1_struct_0(X6))))|~(v20_waybel_0(X8,X6,X7)))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7)))))|(v3_struct_0(X7)|~(l1_orders_2(X7))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))&(((((m1_subset_1(esk3_3(X6,X7,X8),u1_struct_0(X6))|v20_waybel_0(X8,X6,X7))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7)))))|(v3_struct_0(X7)|~(l1_orders_2(X7))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))&(((((m1_subset_1(esk4_3(X6,X7,X8),u1_struct_0(X6))|v20_waybel_0(X8,X6,X7))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7)))))|(v3_struct_0(X7)|~(l1_orders_2(X7))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))&((((~(r4_waybel_0(X6,X7,X8,k2_struct_0(X6,esk3_3(X6,X7,X8),esk4_3(X6,X7,X8))))|v20_waybel_0(X8,X6,X7))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,u1_struct_0(X6),u1_struct_0(X7))))|~(m2_relset_1(X8,u1_struct_0(X6),u1_struct_0(X7)))))|(v3_struct_0(X7)|~(l1_orders_2(X7))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))))),inference(distribute,[status(thm)],[120])).
% cnf(122,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v20_waybel_0(X3,X1,X2)|~l1_orders_2(X1)|~l1_orders_2(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)|~r4_waybel_0(X1,X2,X3,k2_struct_0(X1,esk3_3(X1,X2,X3),esk4_3(X1,X2,X3)))),inference(split_conjunct,[status(thm)],[121])).
% cnf(123,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v20_waybel_0(X3,X1,X2)|m1_subset_1(esk4_3(X1,X2,X3),u1_struct_0(X1))|~l1_orders_2(X1)|~l1_orders_2(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)),inference(split_conjunct,[status(thm)],[121])).
% cnf(124,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v20_waybel_0(X3,X1,X2)|m1_subset_1(esk3_3(X1,X2,X3),u1_struct_0(X1))|~l1_orders_2(X1)|~l1_orders_2(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)),inference(split_conjunct,[status(thm)],[121])).
% fof(126, plain,![X1]:((v3_struct_0(X1)|~(l1_orders_2(X1)))|![X2]:((v3_struct_0(X2)|~(l1_orders_2(X2)))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))))|~(m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))))|((~(v4_waybel34(X3,X1,X2))|![X4]:((~(v1_finset_1(X4))|~(m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))))|r4_waybel_0(X1,X2,X3,X4)))&(?[X4]:((v1_finset_1(X4)&m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1))))&~(r4_waybel_0(X1,X2,X3,X4)))|v4_waybel34(X3,X1,X2)))))),inference(fof_nnf,[status(thm)],[87])).
% fof(127, plain,![X5]:((v3_struct_0(X5)|~(l1_orders_2(X5)))|![X6]:((v3_struct_0(X6)|~(l1_orders_2(X6)))|![X7]:(((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6))))|((~(v4_waybel34(X7,X5,X6))|![X8]:((~(v1_finset_1(X8))|~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X5)))))|r4_waybel_0(X5,X6,X7,X8)))&(?[X9]:((v1_finset_1(X9)&m1_subset_1(X9,k1_zfmisc_1(u1_struct_0(X5))))&~(r4_waybel_0(X5,X6,X7,X9)))|v4_waybel34(X7,X5,X6)))))),inference(variable_rename,[status(thm)],[126])).
% fof(128, plain,![X5]:((v3_struct_0(X5)|~(l1_orders_2(X5)))|![X6]:((v3_struct_0(X6)|~(l1_orders_2(X6)))|![X7]:(((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6))))|((~(v4_waybel34(X7,X5,X6))|![X8]:((~(v1_finset_1(X8))|~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X5)))))|r4_waybel_0(X5,X6,X7,X8)))&(((v1_finset_1(esk5_3(X5,X6,X7))&m1_subset_1(esk5_3(X5,X6,X7),k1_zfmisc_1(u1_struct_0(X5))))&~(r4_waybel_0(X5,X6,X7,esk5_3(X5,X6,X7))))|v4_waybel34(X7,X5,X6)))))),inference(skolemize,[status(esa)],[127])).
% fof(129, plain,![X5]:![X6]:![X7]:![X8]:(((((((~(v1_finset_1(X8))|~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X5)))))|r4_waybel_0(X5,X6,X7,X8))|~(v4_waybel34(X7,X5,X6)))&(((v1_finset_1(esk5_3(X5,X6,X7))&m1_subset_1(esk5_3(X5,X6,X7),k1_zfmisc_1(u1_struct_0(X5))))&~(r4_waybel_0(X5,X6,X7,esk5_3(X5,X6,X7))))|v4_waybel34(X7,X5,X6)))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6)))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))|(v3_struct_0(X5)|~(l1_orders_2(X5)))),inference(shift_quantors,[status(thm)],[128])).
% fof(130, plain,![X5]:![X6]:![X7]:![X8]:(((((((~(v1_finset_1(X8))|~(m1_subset_1(X8,k1_zfmisc_1(u1_struct_0(X5)))))|r4_waybel_0(X5,X6,X7,X8))|~(v4_waybel34(X7,X5,X6)))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6)))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))|(v3_struct_0(X5)|~(l1_orders_2(X5))))&((((((v1_finset_1(esk5_3(X5,X6,X7))|v4_waybel34(X7,X5,X6))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6)))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))|(v3_struct_0(X5)|~(l1_orders_2(X5))))&((((m1_subset_1(esk5_3(X5,X6,X7),k1_zfmisc_1(u1_struct_0(X5)))|v4_waybel34(X7,X5,X6))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6)))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))|(v3_struct_0(X5)|~(l1_orders_2(X5)))))&((((~(r4_waybel_0(X5,X6,X7,esk5_3(X5,X6,X7)))|v4_waybel34(X7,X5,X6))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,u1_struct_0(X5),u1_struct_0(X6))))|~(m2_relset_1(X7,u1_struct_0(X5),u1_struct_0(X6)))))|(v3_struct_0(X6)|~(l1_orders_2(X6))))|(v3_struct_0(X5)|~(l1_orders_2(X5)))))),inference(distribute,[status(thm)],[129])).
% cnf(134,plain,(v3_struct_0(X1)|v3_struct_0(X2)|r4_waybel_0(X1,X2,X3,X4)|~l1_orders_2(X1)|~l1_orders_2(X2)|~m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2))|~v1_funct_1(X3)|~v4_waybel34(X3,X1,X2)|~m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))|~v1_finset_1(X4)),inference(split_conjunct,[status(thm)],[130])).
% fof(145, plain,![X1]:(~(l1_orders_2(X1))|l1_struct_0(X1)),inference(fof_nnf,[status(thm)],[9])).
% fof(146, plain,![X2]:(~(l1_orders_2(X2))|l1_struct_0(X2)),inference(variable_rename,[status(thm)],[145])).
% cnf(147,plain,(l1_struct_0(X1)|~l1_orders_2(X1)),inference(split_conjunct,[status(thm)],[146])).
% fof(191, plain,![X1]:![X2]:![X3]:((((v3_struct_0(X1)|~(l1_struct_0(X1)))|~(m1_subset_1(X2,u1_struct_0(X1))))|~(m1_subset_1(X3,u1_struct_0(X1))))|m1_subset_1(k2_struct_0(X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[93])).
% fof(192, plain,![X4]:![X5]:![X6]:((((v3_struct_0(X4)|~(l1_struct_0(X4)))|~(m1_subset_1(X5,u1_struct_0(X4))))|~(m1_subset_1(X6,u1_struct_0(X4))))|m1_subset_1(k2_struct_0(X4,X5,X6),k1_zfmisc_1(u1_struct_0(X4)))),inference(variable_rename,[status(thm)],[191])).
% cnf(193,plain,(m1_subset_1(k2_struct_0(X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1)))|v3_struct_0(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~m1_subset_1(X2,u1_struct_0(X1))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[192])).
% fof(251, plain,![X1]:(~(v1_xboole_0(X1))|v1_finset_1(X1)),inference(fof_nnf,[status(thm)],[34])).
% fof(252, plain,![X2]:(~(v1_xboole_0(X2))|v1_finset_1(X2)),inference(variable_rename,[status(thm)],[251])).
% cnf(253,plain,(v1_finset_1(X1)|~v1_xboole_0(X1)),inference(split_conjunct,[status(thm)],[252])).
% fof(254, plain,![X1]:(~(l1_struct_0(X1))|m1_subset_1(k1_pre_topc(X1),k1_zfmisc_1(u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[35])).
% fof(255, plain,![X2]:(~(l1_struct_0(X2))|m1_subset_1(k1_pre_topc(X2),k1_zfmisc_1(u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[254])).
% cnf(256,plain,(m1_subset_1(k1_pre_topc(X1),k1_zfmisc_1(u1_struct_0(X1)))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[255])).
% fof(261, plain,![X1]:![X2]:![X3]:((((v3_struct_0(X1)|~(l1_struct_0(X1)))|~(m1_subset_1(X2,u1_struct_0(X1))))|~(m1_subset_1(X3,u1_struct_0(X1))))|k2_struct_0(X1,X2,X3)=k2_tarski(X2,X3)),inference(fof_nnf,[status(thm)],[98])).
% fof(262, plain,![X4]:![X5]:![X6]:((((v3_struct_0(X4)|~(l1_struct_0(X4)))|~(m1_subset_1(X5,u1_struct_0(X4))))|~(m1_subset_1(X6,u1_struct_0(X4))))|k2_struct_0(X4,X5,X6)=k2_tarski(X5,X6)),inference(variable_rename,[status(thm)],[261])).
% cnf(263,plain,(k2_struct_0(X1,X2,X3)=k2_tarski(X2,X3)|v3_struct_0(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~m1_subset_1(X2,u1_struct_0(X1))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[262])).
% fof(294, plain,![X3]:![X4]:(~(v1_xboole_0(k2_tarski(X3,X4)))&v1_finset_1(k2_tarski(X3,X4))),inference(variable_rename,[status(thm)],[99])).
% cnf(295,plain,(v1_finset_1(k2_tarski(X1,X2))),inference(split_conjunct,[status(thm)],[294])).
% fof(420, plain,![X1]:(~(l1_struct_0(X1))|(((((v1_xboole_0(k1_pre_topc(X1))&v1_membered(k1_pre_topc(X1)))&v2_membered(k1_pre_topc(X1)))&v3_membered(k1_pre_topc(X1)))&v4_membered(k1_pre_topc(X1)))&v5_membered(k1_pre_topc(X1)))),inference(fof_nnf,[status(thm)],[70])).
% fof(421, plain,![X2]:(~(l1_struct_0(X2))|(((((v1_xboole_0(k1_pre_topc(X2))&v1_membered(k1_pre_topc(X2)))&v2_membered(k1_pre_topc(X2)))&v3_membered(k1_pre_topc(X2)))&v4_membered(k1_pre_topc(X2)))&v5_membered(k1_pre_topc(X2)))),inference(variable_rename,[status(thm)],[420])).
% fof(422, plain,![X2]:((((((v1_xboole_0(k1_pre_topc(X2))|~(l1_struct_0(X2)))&(v1_membered(k1_pre_topc(X2))|~(l1_struct_0(X2))))&(v2_membered(k1_pre_topc(X2))|~(l1_struct_0(X2))))&(v3_membered(k1_pre_topc(X2))|~(l1_struct_0(X2))))&(v4_membered(k1_pre_topc(X2))|~(l1_struct_0(X2))))&(v5_membered(k1_pre_topc(X2))|~(l1_struct_0(X2)))),inference(distribute,[status(thm)],[421])).
% cnf(428,plain,(v1_xboole_0(k1_pre_topc(X1))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[422])).
% fof(482, negated_conjecture,?[X1]:((~(v3_struct_0(X1))&l1_orders_2(X1))&?[X2]:((~(v3_struct_0(X2))&l1_orders_2(X2))&?[X3]:(((v1_funct_1(X3)&v1_funct_2(X3,u1_struct_0(X1),u1_struct_0(X2)))&m2_relset_1(X3,u1_struct_0(X1),u1_struct_0(X2)))&(v4_waybel34(X3,X1,X2)&(~(v20_waybel_0(X3,X1,X2))|~(v5_waybel34(X3,X1,X2))))))),inference(fof_nnf,[status(thm)],[104])).
% fof(483, negated_conjecture,?[X4]:((~(v3_struct_0(X4))&l1_orders_2(X4))&?[X5]:((~(v3_struct_0(X5))&l1_orders_2(X5))&?[X6]:(((v1_funct_1(X6)&v1_funct_2(X6,u1_struct_0(X4),u1_struct_0(X5)))&m2_relset_1(X6,u1_struct_0(X4),u1_struct_0(X5)))&(v4_waybel34(X6,X4,X5)&(~(v20_waybel_0(X6,X4,X5))|~(v5_waybel34(X6,X4,X5))))))),inference(variable_rename,[status(thm)],[482])).
% fof(484, negated_conjecture,((~(v3_struct_0(esk22_0))&l1_orders_2(esk22_0))&((~(v3_struct_0(esk23_0))&l1_orders_2(esk23_0))&(((v1_funct_1(esk24_0)&v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0)))&m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0)))&(v4_waybel34(esk24_0,esk22_0,esk23_0)&(~(v20_waybel_0(esk24_0,esk22_0,esk23_0))|~(v5_waybel34(esk24_0,esk22_0,esk23_0))))))),inference(skolemize,[status(esa)],[483])).
% cnf(485,negated_conjecture,(~v5_waybel34(esk24_0,esk22_0,esk23_0)|~v20_waybel_0(esk24_0,esk22_0,esk23_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(486,negated_conjecture,(v4_waybel34(esk24_0,esk22_0,esk23_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(487,negated_conjecture,(m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))),inference(split_conjunct,[status(thm)],[484])).
% cnf(488,negated_conjecture,(v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))),inference(split_conjunct,[status(thm)],[484])).
% cnf(489,negated_conjecture,(v1_funct_1(esk24_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(490,negated_conjecture,(l1_orders_2(esk23_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(491,negated_conjecture,(~v3_struct_0(esk23_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(492,negated_conjecture,(l1_orders_2(esk22_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(493,negated_conjecture,(~v3_struct_0(esk22_0)),inference(split_conjunct,[status(thm)],[484])).
% cnf(577,plain,(v1_finset_1(k1_pre_topc(X1))|~l1_struct_0(X1)),inference(spm,[status(thm)],[253,428,theory(equality)])).
% cnf(1110,plain,(m1_subset_1(k2_tarski(X2,X3),k1_zfmisc_1(u1_struct_0(X1)))|v3_struct_0(X1)|~l1_struct_0(X1)|~m1_subset_1(X3,u1_struct_0(X1))|~m1_subset_1(X2,u1_struct_0(X1))),inference(spm,[status(thm)],[193,263,theory(equality)])).
% cnf(1309,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|~v4_waybel34(esk24_0,esk22_0,esk23_0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(spm,[status(thm)],[134,488,theory(equality)])).
% cnf(1310,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[1309,486,theory(equality)])).
% cnf(1311,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|$false|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[1310,489,theory(equality)])).
% cnf(1312,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|$false|$false|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[1311,487,theory(equality)])).
% cnf(1313,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|$false|$false|$false|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[1312,490,theory(equality)])).
% cnf(1314,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|$false|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))|$false|$false|$false|$false),inference(rw,[status(thm)],[1313,492,theory(equality)])).
% cnf(1315,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(cn,[status(thm)],[1314,theory(equality)])).
% cnf(1316,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|v3_struct_0(esk23_0)|~v1_finset_1(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[1315,493,theory(equality)])).
% cnf(1317,negated_conjecture,(r4_waybel_0(esk22_0,esk23_0,esk24_0,X1)|~v1_finset_1(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[1316,491,theory(equality)])).
% cnf(1327,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(spm,[status(thm)],[115,1317,theory(equality)])).
% cnf(1328,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|$false|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[1327,488,theory(equality)])).
% cnf(1329,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|$false|$false|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[1328,489,theory(equality)])).
% cnf(1330,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|$false|$false|$false|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[1329,487,theory(equality)])).
% cnf(1331,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|$false|$false|$false|$false|~l1_orders_2(esk22_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[1330,490,theory(equality)])).
% cnf(1332,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|$false|$false|$false|$false|$false|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[1331,492,theory(equality)])).
% cnf(1333,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(cn,[status(thm)],[1332,theory(equality)])).
% cnf(1334,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[1333,493,theory(equality)])).
% cnf(1335,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~m1_subset_1(k1_pre_topc(esk22_0),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[1334,491,theory(equality)])).
% cnf(1377,plain,(v20_waybel_0(X1,X2,X3)|v3_struct_0(X2)|v3_struct_0(X3)|~r4_waybel_0(X2,X3,X1,k2_tarski(esk3_3(X2,X3,X1),esk4_3(X2,X3,X1)))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~m2_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~l1_orders_2(X3)|~l1_orders_2(X2)|~l1_struct_0(X2)|~m1_subset_1(esk4_3(X2,X3,X1),u1_struct_0(X2))|~m1_subset_1(esk3_3(X2,X3,X1),u1_struct_0(X2))),inference(spm,[status(thm)],[122,263,theory(equality)])).
% cnf(1411,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|~v1_finset_1(k1_pre_topc(esk22_0))|~l1_struct_0(esk22_0)),inference(spm,[status(thm)],[1335,256,theory(equality)])).
% cnf(1421,negated_conjecture,(v5_waybel34(esk24_0,esk22_0,esk23_0)|~l1_struct_0(esk22_0)),inference(csr,[status(thm)],[1411,577])).
% cnf(1422,negated_conjecture,(~v20_waybel_0(esk24_0,esk22_0,esk23_0)|~l1_struct_0(esk22_0)),inference(spm,[status(thm)],[485,1421,theory(equality)])).
% cnf(7024,plain,(v20_waybel_0(X1,X2,X3)|v3_struct_0(X2)|v3_struct_0(X3)|~l1_struct_0(X2)|~m1_subset_1(esk4_3(X2,X3,X1),u1_struct_0(X2))|~r4_waybel_0(X2,X3,X1,k2_tarski(esk3_3(X2,X3,X1),esk4_3(X2,X3,X1)))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~m2_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(csr,[status(thm)],[1377,124])).
% cnf(7025,plain,(v20_waybel_0(X1,X2,X3)|v3_struct_0(X2)|v3_struct_0(X3)|~l1_struct_0(X2)|~r4_waybel_0(X2,X3,X1,k2_tarski(esk3_3(X2,X3,X1),esk4_3(X2,X3,X1)))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~m2_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(csr,[status(thm)],[7024,123])).
% cnf(7026,plain,(v20_waybel_0(X1,X2,X3)|v3_struct_0(X2)|v3_struct_0(X3)|~r4_waybel_0(X2,X3,X1,k2_tarski(esk3_3(X2,X3,X1),esk4_3(X2,X3,X1)))|~v1_funct_2(X1,u1_struct_0(X2),u1_struct_0(X3))|~v1_funct_1(X1)|~m2_relset_1(X1,u1_struct_0(X2),u1_struct_0(X3))|~l1_orders_2(X3)|~l1_orders_2(X2)),inference(csr,[status(thm)],[7025,147])).
% cnf(7027,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|~v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(spm,[status(thm)],[7026,1317,theory(equality)])).
% cnf(7029,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7027,488,theory(equality)])).
% cnf(7030,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|$false|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7029,489,theory(equality)])).
% cnf(7031,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|$false|$false|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7030,487,theory(equality)])).
% cnf(7032,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|$false|$false|$false|~l1_orders_2(esk22_0)|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7031,490,theory(equality)])).
% cnf(7033,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|$false|$false|$false|$false|~v1_finset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)))|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7032,492,theory(equality)])).
% cnf(7034,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|$false|$false|$false|$false|$false|$false|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(rw,[status(thm)],[7033,295,theory(equality)])).
% cnf(7035,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|v3_struct_0(esk22_0)|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(cn,[status(thm)],[7034,theory(equality)])).
% cnf(7036,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[7035,491,theory(equality)])).
% cnf(7037,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|~m1_subset_1(k2_tarski(esk3_3(esk22_0,esk23_0,esk24_0),esk4_3(esk22_0,esk23_0,esk24_0)),k1_zfmisc_1(u1_struct_0(esk22_0)))),inference(sr,[status(thm)],[7036,493,theory(equality)])).
% cnf(8396,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk4_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(spm,[status(thm)],[7037,1110,theory(equality)])).
% cnf(8397,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk4_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(sr,[status(thm)],[8396,493,theory(equality)])).
% cnf(8402,negated_conjecture,(~l1_struct_0(esk22_0)|~m1_subset_1(esk4_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(csr,[status(thm)],[8397,1422])).
% cnf(8403,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|~v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(spm,[status(thm)],[8402,123,theory(equality)])).
% cnf(8404,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|$false|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8403,488,theory(equality)])).
% cnf(8405,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|$false|$false|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8404,489,theory(equality)])).
% cnf(8406,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|$false|$false|$false|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8405,487,theory(equality)])).
% cnf(8407,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|$false|$false|$false|$false|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8406,490,theory(equality)])).
% cnf(8408,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[8407,492,theory(equality)])).
% cnf(8409,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(cn,[status(thm)],[8408,theory(equality)])).
% cnf(8410,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(sr,[status(thm)],[8409,493,theory(equality)])).
% cnf(8411,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(sr,[status(thm)],[8410,491,theory(equality)])).
% cnf(8412,negated_conjecture,(~l1_struct_0(esk22_0)|~m1_subset_1(esk3_3(esk22_0,esk23_0,esk24_0),u1_struct_0(esk22_0))),inference(csr,[status(thm)],[8411,1422])).
% cnf(8413,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|~v1_funct_2(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(spm,[status(thm)],[8412,124,theory(equality)])).
% cnf(8414,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|$false|~v1_funct_1(esk24_0)|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8413,488,theory(equality)])).
% cnf(8415,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|$false|$false|~m2_relset_1(esk24_0,u1_struct_0(esk22_0),u1_struct_0(esk23_0))|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8414,489,theory(equality)])).
% cnf(8416,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|$false|$false|$false|~l1_orders_2(esk23_0)|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8415,487,theory(equality)])).
% cnf(8417,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|$false|$false|$false|$false|~l1_orders_2(esk22_0)),inference(rw,[status(thm)],[8416,490,theory(equality)])).
% cnf(8418,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[8417,492,theory(equality)])).
% cnf(8419,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk22_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)),inference(cn,[status(thm)],[8418,theory(equality)])).
% cnf(8420,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|v3_struct_0(esk23_0)|~l1_struct_0(esk22_0)),inference(sr,[status(thm)],[8419,493,theory(equality)])).
% cnf(8421,negated_conjecture,(v20_waybel_0(esk24_0,esk22_0,esk23_0)|~l1_struct_0(esk22_0)),inference(sr,[status(thm)],[8420,491,theory(equality)])).
% cnf(8422,negated_conjecture,(~l1_struct_0(esk22_0)),inference(csr,[status(thm)],[8421,1422])).
% cnf(8423,negated_conjecture,(~l1_orders_2(esk22_0)),inference(spm,[status(thm)],[8422,147,theory(equality)])).
% cnf(8424,negated_conjecture,($false),inference(rw,[status(thm)],[8423,492,theory(equality)])).
% cnf(8425,negated_conjecture,($false),inference(cn,[status(thm)],[8424,theory(equality)])).
% cnf(8426,negated_conjecture,($false),8425,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3676
% # ...of these trivial : 0
% # ...subsumed : 2231
% # ...remaining for further processing: 1445
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 23
% # Backward-rewritten : 19
% # Generated clauses : 5373
% # ...of the previous two non-trivial : 5156
% # Contextual simplify-reflections : 1766
% # Paramodulations : 5342
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1388
% # Positive orientable unit clauses: 52
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 13
% # Non-unit-clauses : 1322
% # Current number of unprocessed clauses: 1593
% # ...number of literals in the above : 6220
% # Clause-clause subsumption calls (NU) : 109642
% # Rec. Clause-clause subsumption calls : 75338
% # Unit Clause-clause subsumption calls : 2343
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 12
% # Indexed BW rewrite successes : 12
% # Backwards rewriting index: 612 leaves, 1.42+/-1.222 terms/leaf
% # Paramod-from index: 286 leaves, 1.26+/-1.052 terms/leaf
% # Paramod-into index: 500 leaves, 1.38+/-1.179 terms/leaf
% # -------------------------------------------------
% # User time : 0.567 s
% # System time : 0.019 s
% # Total time : 0.586 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.75 CPU 0.85 WC
% FINAL PrfWatch: 0.75 CPU 0.85 WC
% SZS output end Solution for /tmp/SystemOnTPTP24563/LAT379+1.tptp
%
%------------------------------------------------------------------------------