%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT379+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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 : 600s
% DateTime : Sun Jul 17 06:51:44 EDT 2022
% Result : Theorem 2.53s 2.74s
% Output : Refutation 2.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 34
% Syntax : Number of clauses : 72 ( 42 unt; 14 nHn; 72 RR)
% Number of literals : 201 ( 0 equ; 114 neg)
% Maximal clause size : 13 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v1_funct_1(skc14),
file('LAT379+1.p',unknown),
[] ).
cnf(2,axiom,
l1_orders_2(skc12),
file('LAT379+1.p',unknown),
[] ).
cnf(3,axiom,
l1_orders_2(skc13),
file('LAT379+1.p',unknown),
[] ).
cnf(6,axiom,
v1_xboole_0(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(7,axiom,
v1_membered(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(8,axiom,
v2_membered(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(9,axiom,
v3_membered(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(10,axiom,
v4_membered(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(11,axiom,
v5_membered(k1_xboole_0),
file('LAT379+1.p',unknown),
[] ).
cnf(21,axiom,
v1_relat_1(skc24),
file('LAT379+1.p',unknown),
[] ).
cnf(22,axiom,
v1_xboole_0(skc24),
file('LAT379+1.p',unknown),
[] ).
cnf(23,axiom,
v1_funct_1(skc24),
file('LAT379+1.p',unknown),
[] ).
cnf(28,axiom,
~ v3_struct_0(skc13),
file('LAT379+1.p',unknown),
[] ).
cnf(29,axiom,
~ v3_struct_0(skc12),
file('LAT379+1.p',unknown),
[] ).
cnf(35,axiom,
v4_waybel34(skc14,skc12,skc13),
file('LAT379+1.p',unknown),
[] ).
cnf(37,axiom,
v1_finset_1(k2_tarski(u,v)),
file('LAT379+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ l1_orders_2(u)
| l1_struct_0(u) ),
file('LAT379+1.p',unknown),
[] ).
cnf(56,axiom,
v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13)),
file('LAT379+1.p',unknown),
[] ).
cnf(57,axiom,
m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13)),
file('LAT379+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ l1_orders_2(u)
| v1_xboole_0(k1_pre_topc(u)) ),
file('LAT379+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ l1_orders_2(u)
| v1_finset_1(k1_pre_topc(u)) ),
file('LAT379+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ v1_xboole_0(u)
| equal(u,k1_xboole_0) ),
file('LAT379+1.p',unknown),
[] ).
cnf(88,axiom,
( ~ l1_struct_0(u)
| equal(k1_pre_topc(u),k1_xboole_0) ),
file('LAT379+1.p',unknown),
[] ).
cnf(89,axiom,
m1_subset_1(skf14(u,v,w),u1_struct_0(w)),
file('LAT379+1.p',unknown),
[] ).
cnf(90,axiom,
m1_subset_1(skf13(u,v,w),u1_struct_0(w)),
file('LAT379+1.p',unknown),
[] ).
cnf(124,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| v1_relat_1(u) ),
file('LAT379+1.p',unknown),
[] ).
cnf(125,axiom,
( ~ l1_struct_0(u)
| m1_subset_1(k1_pre_topc(u),k1_zfmisc_1(u1_struct_0(u))) ),
file('LAT379+1.p',unknown),
[] ).
cnf(136,axiom,
( ~ v5_waybel34(skc14,skc12,skc13)
| ~ v20_waybel_0(skc14,skc12,skc13) ),
file('LAT379+1.p',unknown),
[] ).
cnf(170,axiom,
( ~ m2_relset_1(u,v,w)
| m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w))) ),
file('LAT379+1.p',unknown),
[] ).
cnf(174,axiom,
( ~ l1_struct_0(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_subset_1(w,u1_struct_0(u))
| v3_struct_0(u)
| equal(k2_struct_0(u,v,w),k2_tarski(v,w)) ),
file('LAT379+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ l1_struct_0(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_subset_1(w,u1_struct_0(u))
| m1_subset_1(k2_struct_0(u,w,v),k1_zfmisc_1(u1_struct_0(u)))
| v3_struct_0(u) ),
file('LAT379+1.p',unknown),
[] ).
cnf(177,axiom,
( ~ v1_funct_1(u)
| ~ l1_orders_2(v)
| ~ l1_orders_2(w)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ r4_waybel_0(w,v,u,k1_pre_topc(w))
| v3_struct_0(v)
| v3_struct_0(w)
| v5_waybel34(u,w,v) ),
file('LAT379+1.p',unknown),
[] ).
cnf(181,axiom,
( ~ v1_funct_1(u)
| ~ l1_orders_2(v)
| ~ l1_orders_2(w)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ r4_waybel_0(w,v,u,k2_struct_0(w,skf13(u,v,w),skf14(u,v,w)))
| v3_struct_0(v)
| v3_struct_0(w)
| v20_waybel_0(u,w,v) ),
file('LAT379+1.p',unknown),
[] ).
cnf(182,axiom,
( ~ v1_funct_1(u)
| ~ l1_orders_2(v)
| ~ l1_orders_2(w)
| ~ v1_finset_1(x)
| ~ m1_subset_1(x,k1_zfmisc_1(u1_struct_0(w)))
| ~ v4_waybel34(u,w,v)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| v3_struct_0(v)
| v3_struct_0(w)
| r4_waybel_0(w,v,u,x) ),
file('LAT379+1.p',unknown),
[] ).
cnf(190,plain,
( ~ l1_struct_0(u)
| m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(u))) ),
inference(rew,[status(thm),theory(equality)],[88,125]),
[iquote('0:Rew:88.1,125.1')] ).
cnf(192,plain,
( ~ l1_struct_0(u)
| ~ m1_subset_1(v,u1_struct_0(u))
| ~ m1_subset_1(w,u1_struct_0(u))
| v3_struct_0(u)
| m1_subset_1(k2_tarski(v,w),k1_zfmisc_1(u1_struct_0(u))) ),
inference(rew,[status(thm),theory(equality)],[174,175]),
[iquote('0:Rew:174.3,175.3')] ).
cnf(212,plain,
v1_xboole_0(k1_pre_topc(skc13)),
inference(res,[status(thm),theory(equality)],[3,73]),
[iquote('0:Res:3.0,73.0')] ).
cnf(213,plain,
v1_finset_1(k1_pre_topc(skc13)),
inference(res,[status(thm),theory(equality)],[3,74]),
[iquote('0:Res:3.0,74.0')] ).
cnf(219,plain,
l1_struct_0(skc13),
inference(res,[status(thm),theory(equality)],[3,50]),
[iquote('0:Res:3.0,50.0')] ).
cnf(246,plain,
v1_xboole_0(k1_pre_topc(skc12)),
inference(res,[status(thm),theory(equality)],[2,73]),
[iquote('0:Res:2.0,73.0')] ).
cnf(253,plain,
l1_struct_0(skc12),
inference(res,[status(thm),theory(equality)],[2,50]),
[iquote('0:Res:2.0,50.0')] ).
cnf(326,plain,
( ~ l1_orders_2(skc12)
| ~ l1_orders_2(skc13)
| ~ v1_funct_1(skc14)
| ~ r4_waybel_0(skc12,skc13,skc14,k1_pre_topc(skc12))
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| v5_waybel34(skc14,skc12,skc13)
| v3_struct_0(skc12)
| v3_struct_0(skc13) ),
inference(res,[status(thm),theory(equality)],[56,177]),
[iquote('0:Res:56.0,177.4')] ).
cnf(327,plain,
( ~ v1_finset_1(u)
| ~ l1_orders_2(skc12)
| ~ l1_orders_2(skc13)
| ~ v1_funct_1(skc14)
| ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc12)))
| ~ v4_waybel34(skc14,skc12,skc13)
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| r4_waybel_0(skc12,skc13,skc14,u)
| v3_struct_0(skc12)
| v3_struct_0(skc13) ),
inference(res,[status(thm),theory(equality)],[56,182]),
[iquote('0:Res:56.0,182.6')] ).
cnf(342,plain,
( ~ r4_waybel_0(skc12,skc13,skc14,k1_pre_topc(skc12))
| v5_waybel34(skc14,skc12,skc13) ),
inference(mrr,[status(thm)],[326,2,3,1,57,29,28]),
[iquote('0:MRR:326.0,326.1,326.2,326.4,326.6,326.7,2.0,3.0,1.0,57.0,29.0,28.0')] ).
cnf(360,plain,
( ~ v1_finset_1(u)
| ~ m1_subset_1(u,k1_zfmisc_1(u1_struct_0(skc12)))
| r4_waybel_0(skc12,skc13,skc14,u) ),
inference(mrr,[status(thm)],[327,2,3,1,35,57,29,28]),
[iquote('0:MRR:327.1,327.2,327.3,327.5,327.6,327.8,327.9,2.0,3.0,1.0,35.0,57.0,29.0,28.0')] ).
cnf(475,plain,
~ v5_waybel34(skc14,skc12,skc13),
inference(spt,[spt(split,[position(s1)])],[136]),
[iquote('1:Spt:136.0')] ).
cnf(476,plain,
~ r4_waybel_0(skc12,skc13,skc14,k1_pre_topc(skc12)),
inference(mrr,[status(thm)],[342,475]),
[iquote('1:MRR:342.1,475.0')] ).
cnf(477,plain,
equal(k1_pre_topc(skc13),k1_xboole_0),
inference(ems,[status(thm)],[86,212]),
[iquote('0:EmS:86.0,212.0')] ).
cnf(478,plain,
equal(k1_pre_topc(skc12),k1_xboole_0),
inference(ems,[status(thm)],[86,246]),
[iquote('0:EmS:86.0,246.0')] ).
cnf(480,plain,
equal(skc24,k1_xboole_0),
inference(ems,[status(thm)],[86,22]),
[iquote('0:EmS:86.0,22.0')] ).
cnf(481,plain,
v1_relat_1(k1_xboole_0),
inference(rew,[status(thm),theory(equality)],[480,21]),
[iquote('0:Rew:480.0,21.0')] ).
cnf(483,plain,
v1_funct_1(k1_xboole_0),
inference(rew,[status(thm),theory(equality)],[480,23]),
[iquote('0:Rew:480.0,23.0')] ).
cnf(489,plain,
v1_finset_1(k1_xboole_0),
inference(rew,[status(thm),theory(equality)],[477,213]),
[iquote('0:Rew:477.0,213.0')] ).
cnf(522,plain,
~ r4_waybel_0(skc12,skc13,skc14,k1_xboole_0),
inference(rew,[status(thm),theory(equality)],[478,476]),
[iquote('1:Rew:478.0,476.0')] ).
cnf(1200,plain,
( ~ m2_relset_1(u,v,w)
| v1_relat_1(u) ),
inference(res,[status(thm),theory(equality)],[170,124]),
[iquote('0:Res:170.1,124.0')] ).
cnf(1375,plain,
( ~ l1_struct_0(u)
| ~ v1_funct_1(v)
| ~ l1_orders_2(w)
| ~ l1_orders_2(u)
| ~ m1_subset_1(skf13(v,w,u),u1_struct_0(u))
| ~ m1_subset_1(skf14(v,w,u),u1_struct_0(u))
| ~ m2_relset_1(v,u1_struct_0(u),u1_struct_0(w))
| ~ v1_funct_2(v,u1_struct_0(u),u1_struct_0(w))
| ~ r4_waybel_0(u,w,v,k2_tarski(skf13(v,w,u),skf14(v,w,u)))
| v3_struct_0(u)
| v3_struct_0(w)
| v3_struct_0(u)
| v20_waybel_0(v,u,w) ),
inference(spl,[status(thm),theory(equality)],[174,181]),
[iquote('0:SpL:174.4,181.5')] ).
cnf(1376,plain,
( ~ l1_struct_0(u)
| ~ v1_funct_1(v)
| ~ l1_orders_2(w)
| ~ l1_orders_2(u)
| ~ m1_subset_1(skf13(v,w,u),u1_struct_0(u))
| ~ m1_subset_1(skf14(v,w,u),u1_struct_0(u))
| ~ m2_relset_1(v,u1_struct_0(u),u1_struct_0(w))
| ~ v1_funct_2(v,u1_struct_0(u),u1_struct_0(w))
| ~ r4_waybel_0(u,w,v,k2_tarski(skf13(v,w,u),skf14(v,w,u)))
| v3_struct_0(w)
| v3_struct_0(u)
| v20_waybel_0(v,u,w) ),
inference(obv,[status(thm),theory(equality)],[1375]),
[iquote('0:Obv:1375.9')] ).
cnf(1377,plain,
( ~ v1_funct_1(u)
| ~ l1_orders_2(v)
| ~ l1_orders_2(w)
| ~ m1_subset_1(skf13(u,v,w),u1_struct_0(w))
| ~ m1_subset_1(skf14(u,v,w),u1_struct_0(w))
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ r4_waybel_0(w,v,u,k2_tarski(skf13(u,v,w),skf14(u,v,w)))
| v3_struct_0(v)
| v3_struct_0(w)
| v20_waybel_0(u,w,v) ),
inference(ssi,[status(thm)],[1376,50]),
[iquote('0:SSi:1376.0,50.1')] ).
cnf(1378,plain,
( ~ v1_funct_1(u)
| ~ l1_orders_2(v)
| ~ l1_orders_2(w)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ r4_waybel_0(w,v,u,k2_tarski(skf13(u,v,w),skf14(u,v,w)))
| v3_struct_0(v)
| v3_struct_0(w)
| v20_waybel_0(u,w,v) ),
inference(mrr,[status(thm)],[1377,90,89]),
[iquote('0:MRR:1377.3,1377.4,90.0,89.0')] ).
cnf(1399,plain,
v1_relat_1(skc14),
inference(res,[status(thm),theory(equality)],[57,1200]),
[iquote('0:Res:57.0,1200.0')] ).
cnf(5393,plain,
( ~ v1_finset_1(k1_xboole_0)
| ~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(skc12))) ),
inference(res,[status(thm),theory(equality)],[360,522]),
[iquote('1:Res:360.2,522.0')] ).
cnf(5396,plain,
~ m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(skc12))),
inference(ssi,[status(thm)],[5393,11,7,10,9,8,6,481,483,489]),
[iquote('1:SSi:5393.0,11.0,7.0,10.0,9.0,8.0,6.0,481.0,483.0,489.0')] ).
cnf(5400,plain,
~ l1_struct_0(skc12),
inference(res,[status(thm),theory(equality)],[190,5396]),
[iquote('1:Res:190.1,5396.0')] ).
cnf(5403,plain,
$false,
inference(ssi,[status(thm)],[5400,2,253]),
[iquote('1:SSi:5400.0,2.0,253.0')] ).
cnf(5404,plain,
v5_waybel34(skc14,skc12,skc13),
inference(spt,[spt(split,[position(sa)])],[5403,475]),
[iquote('1:Spt:5403.0,136.0,475.0')] ).
cnf(5405,plain,
~ v20_waybel_0(skc14,skc12,skc13),
inference(spt,[spt(split,[position(s2)])],[136]),
[iquote('1:Spt:5403.0,136.1')] ).
cnf(9502,plain,
( ~ v1_finset_1(k2_tarski(skf13(skc14,skc13,skc12),skf14(skc14,skc13,skc12)))
| ~ v1_funct_1(skc14)
| ~ l1_orders_2(skc13)
| ~ l1_orders_2(skc12)
| ~ m1_subset_1(k2_tarski(skf13(skc14,skc13,skc12),skf14(skc14,skc13,skc12)),k1_zfmisc_1(u1_struct_0(skc12)))
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| ~ v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| v3_struct_0(skc13)
| v3_struct_0(skc12)
| v20_waybel_0(skc14,skc12,skc13) ),
inference(res,[status(thm),theory(equality)],[360,1378]),
[iquote('0:Res:360.2,1378.5')] ).
cnf(9503,plain,
( ~ m1_subset_1(k2_tarski(skf13(skc14,skc13,skc12),skf14(skc14,skc13,skc12)),k1_zfmisc_1(u1_struct_0(skc12)))
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| ~ v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| v3_struct_0(skc13)
| v3_struct_0(skc12)
| v20_waybel_0(skc14,skc12,skc13) ),
inference(ssi,[status(thm)],[9502,2,253,3,219,1,1399,37]),
[iquote('0:SSi:9502.3,9502.2,9502.1,9502.0,2.0,253.0,3.0,219.0,1.0,1399.0,37.0')] ).
cnf(9504,plain,
~ m1_subset_1(k2_tarski(skf13(skc14,skc13,skc12),skf14(skc14,skc13,skc12)),k1_zfmisc_1(u1_struct_0(skc12))),
inference(mrr,[status(thm)],[9503,57,56,28,29,5405]),
[iquote('1:MRR:9503.1,9503.2,9503.3,9503.4,9503.5,57.0,56.0,28.0,29.0,5405.0')] ).
cnf(10113,plain,
( ~ l1_struct_0(skc12)
| ~ m1_subset_1(skf13(skc14,skc13,skc12),u1_struct_0(skc12))
| ~ m1_subset_1(skf14(skc14,skc13,skc12),u1_struct_0(skc12))
| v3_struct_0(skc12) ),
inference(res,[status(thm),theory(equality)],[192,9504]),
[iquote('1:Res:192.4,9504.0')] ).
cnf(10118,plain,
( ~ m1_subset_1(skf13(skc14,skc13,skc12),u1_struct_0(skc12))
| ~ m1_subset_1(skf14(skc14,skc13,skc12),u1_struct_0(skc12))
| v3_struct_0(skc12) ),
inference(ssi,[status(thm)],[10113,2,253]),
[iquote('1:SSi:10113.0,2.0,253.0')] ).
cnf(10119,plain,
$false,
inference(mrr,[status(thm)],[10118,90,89,29]),
[iquote('1:MRR:10118.0,10118.1,10118.2,90.0,89.0,29.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT379+1 : TPTP v8.1.0. Released v3.4.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n021.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 29 13:30:57 EDT 2022
% 0.12/0.34 % CPUTime :
% 2.53/2.74
% 2.53/2.74 SPASS V 3.9
% 2.53/2.74 SPASS beiseite: Proof found.
% 2.53/2.74 % SZS status Theorem
% 2.53/2.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.53/2.74 SPASS derived 9385 clauses, backtracked 6 clauses, performed 1 splits and kept 5495 clauses.
% 2.53/2.74 SPASS allocated 104393 KBytes.
% 2.53/2.74 SPASS spent 0:00:02.39 on the problem.
% 2.53/2.74 0:00:00.04 for the input.
% 2.53/2.74 0:00:00.04 for the FLOTTER CNF translation.
% 2.53/2.74 0:00:00.12 for inferences.
% 2.53/2.74 0:00:00.00 for the backtracking.
% 2.53/2.74 0:00:01.90 for the reduction.
% 2.53/2.74
% 2.53/2.74
% 2.53/2.74 Here is a proof with depth 3, length 72 :
% 2.53/2.74 % SZS output start Refutation
% See solution above
% 2.53/2.79 Formulae used in the proof : t65_waybel34 fc6_membered rc2_funct_1 fc2_finset_1 dt_l1_orders_2 fc1_waybel_0 t6_boole d2_pre_topc d35_waybel_0 existence_m1_subset_1 cc1_relset_1 dt_k1_pre_topc dt_m2_relset_1 redefinition_k2_struct_0 dt_k2_struct_0 d16_waybel34 d15_waybel34 rc1_finset_1
% 2.53/2.79
%------------------------------------------------------------------------------