%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SEU441+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %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 : 600s
% DateTime : Tue Jul 19 14:37:32 EDT 2022
% Result : Theorem 3.30s 3.52s
% Output : Refutation 3.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of clauses : 55 ( 22 unt; 0 nHn; 55 RR)
% Number of literals : 102 ( 0 equ; 56 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-5 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(14,axiom,
m2_relset_1(skc12,skc9,skc11),
file('SEU441+1.p',unknown),
[] ).
cnf(15,axiom,
m2_relset_1(skc10,skc8,skc9),
file('SEU441+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ v1_relat_1(u)
| equal(k2_relat_1(u),k2_funct_5(u)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(39,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(v))
| r1_tarski(u,v) ),
file('SEU441+1.p',unknown),
[] ).
cnf(41,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| v1_relat_1(u) ),
file('SEU441+1.p',unknown),
[] ).
cnf(45,axiom,
( ~ m2_relset_1(u,v,w)
| m1_relset_1(u,v,w) ),
file('SEU441+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ m2_relset_1(u,v,w)
| m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w))) ),
file('SEU441+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ m1_relset_1(u,v,w)
| m1_subset_1(k5_relset_1(v,w,u),k1_zfmisc_1(w)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(57,axiom,
( ~ m1_relset_1(u,v,w)
| equal(k5_relset_1(v,w,u),k2_relat_1(u)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ m2_relset_1(u,v,w)
| equal(k10_relset_1(v,w,u,v),k2_funct_5(u)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ m1_relset_1(u,v,w)
| equal(k10_relset_1(v,w,u,x),k9_relat_1(u,x)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ v1_relat_1(u)
| ~ r1_tarski(v,w)
| r1_tarski(k9_relat_1(u,v),k9_relat_1(u,w)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ v1_relat_1(u)
| ~ v1_relat_1(v)
| equal(k9_relat_1(k5_relat_1(u,v),w),k9_relat_1(v,k9_relat_1(u,w))) ),
file('SEU441+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| ~ m1_subset_1(x,k1_zfmisc_1(k2_zfmisc_1(w,y)))
| m2_relset_1(k9_relset_2(v,w,y,u,x),v,y) ),
file('SEU441+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| ~ m1_subset_1(x,k1_zfmisc_1(k2_zfmisc_1(y,v)))
| equal(k9_relset_2(y,v,w,x,u),k5_relat_1(x,u)) ),
file('SEU441+1.p',unknown),
[] ).
cnf(70,axiom,
( ~ r1_tarski(k2_funct_5(k9_relset_2(skc8,skc9,skc11,skc10,skc12)),k2_funct_5(skc12))
| ~ equal(k2_funct_5(k9_relset_2(skc8,skc9,skc11,skc10,skc12)),k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10))) ),
file('SEU441+1.p',unknown),
[] ).
cnf(73,plain,
( ~ m1_relset_1(u,v,w)
| m1_subset_1(k2_relat_1(u),k1_zfmisc_1(w)) ),
inference(rew,[status(thm),theory(equality)],[57,55]),
[iquote('0:Rew:57.1,55.1')] ).
cnf(76,plain,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| ~ m1_subset_1(x,k1_zfmisc_1(k2_zfmisc_1(y,v)))
| m2_relset_1(k5_relat_1(x,u),y,w) ),
inference(rew,[status(thm),theory(equality)],[69,68]),
[iquote('0:Rew:69.2,68.2')] ).
cnf(78,plain,
equal(k10_relset_1(skc8,skc9,skc10,skc8),k2_funct_5(skc10)),
inference(res,[status(thm),theory(equality)],[15,62]),
[iquote('0:Res:15.0,62.0')] ).
cnf(79,plain,
m1_subset_1(skc10,k1_zfmisc_1(k2_zfmisc_1(skc8,skc9))),
inference(res,[status(thm),theory(equality)],[15,54]),
[iquote('0:Res:15.0,54.0')] ).
cnf(80,plain,
m1_relset_1(skc10,skc8,skc9),
inference(res,[status(thm),theory(equality)],[15,45]),
[iquote('0:Res:15.0,45.0')] ).
cnf(82,plain,
equal(k10_relset_1(skc9,skc11,skc12,skc9),k2_funct_5(skc12)),
inference(res,[status(thm),theory(equality)],[14,62]),
[iquote('0:Res:14.0,62.0')] ).
cnf(83,plain,
m1_subset_1(skc12,k1_zfmisc_1(k2_zfmisc_1(skc9,skc11))),
inference(res,[status(thm),theory(equality)],[14,54]),
[iquote('0:Res:14.0,54.0')] ).
cnf(84,plain,
m1_relset_1(skc12,skc9,skc11),
inference(res,[status(thm),theory(equality)],[14,45]),
[iquote('0:Res:14.0,45.0')] ).
cnf(173,plain,
v1_relat_1(skc12),
inference(res,[status(thm),theory(equality)],[83,41]),
[iquote('0:Res:83.0,41.0')] ).
cnf(174,plain,
v1_relat_1(skc10),
inference(res,[status(thm),theory(equality)],[79,41]),
[iquote('0:Res:79.0,41.0')] ).
cnf(295,plain,
m1_subset_1(k2_relat_1(skc10),k1_zfmisc_1(skc9)),
inference(res,[status(thm),theory(equality)],[80,73]),
[iquote('0:Res:80.0,73.0')] ).
cnf(313,plain,
r1_tarski(k2_relat_1(skc10),skc9),
inference(res,[status(thm),theory(equality)],[295,39]),
[iquote('0:Res:295.0,39.0')] ).
cnf(322,plain,
( ~ v1_relat_1(skc10)
| r1_tarski(k2_funct_5(skc10),skc9) ),
inference(spr,[status(thm),theory(equality)],[38,313]),
[iquote('0:SpR:38.1,313.0')] ).
cnf(324,plain,
r1_tarski(k2_funct_5(skc10),skc9),
inference(ssi,[status(thm)],[322,174]),
[iquote('0:SSi:322.0,174.0')] ).
cnf(507,plain,
( ~ m1_relset_1(skc12,skc9,skc11)
| equal(k9_relat_1(skc12,skc9),k2_funct_5(skc12)) ),
inference(spr,[status(thm),theory(equality)],[64,82]),
[iquote('0:SpR:64.1,82.0')] ).
cnf(508,plain,
( ~ m1_relset_1(skc10,skc8,skc9)
| equal(k9_relat_1(skc10,skc8),k2_funct_5(skc10)) ),
inference(spr,[status(thm),theory(equality)],[64,78]),
[iquote('0:SpR:64.1,78.0')] ).
cnf(509,plain,
( ~ m1_relset_1(u,v,w)
| ~ m2_relset_1(u,v,w)
| equal(k9_relat_1(u,v),k2_funct_5(u)) ),
inference(spr,[status(thm),theory(equality)],[64,62]),
[iquote('0:SpR:64.1,62.1')] ).
cnf(511,plain,
equal(k9_relat_1(skc12,skc9),k2_funct_5(skc12)),
inference(mrr,[status(thm)],[507,84]),
[iquote('0:MRR:507.0,84.0')] ).
cnf(512,plain,
equal(k9_relat_1(skc10,skc8),k2_funct_5(skc10)),
inference(mrr,[status(thm)],[508,80]),
[iquote('0:MRR:508.0,80.0')] ).
cnf(513,plain,
( ~ m2_relset_1(u,v,w)
| equal(k9_relat_1(u,v),k2_funct_5(u)) ),
inference(mrr,[status(thm)],[509,45]),
[iquote('0:MRR:509.0,45.1')] ).
cnf(514,plain,
( ~ v1_relat_1(skc12)
| ~ r1_tarski(u,skc9)
| r1_tarski(k9_relat_1(skc12,u),k2_funct_5(skc12)) ),
inference(spr,[status(thm),theory(equality)],[511,65]),
[iquote('0:SpR:511.0,65.2')] ).
cnf(521,plain,
( ~ r1_tarski(u,skc9)
| r1_tarski(k9_relat_1(skc12,u),k2_funct_5(skc12)) ),
inference(ssi,[status(thm)],[514,173]),
[iquote('0:SSi:514.0,173.0')] ).
cnf(2026,plain,
( ~ m1_subset_1(skc12,k1_zfmisc_1(k2_zfmisc_1(skc9,skc11)))
| ~ m1_subset_1(skc10,k1_zfmisc_1(k2_zfmisc_1(skc8,skc9)))
| ~ r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12))
| ~ equal(k2_funct_5(k9_relset_2(skc8,skc9,skc11,skc10,skc12)),k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10))) ),
inference(spl,[status(thm),theory(equality)],[69,70]),
[iquote('0:SpL:69.2,70.0')] ).
cnf(2031,plain,
( ~ m1_subset_1(skc12,k1_zfmisc_1(k2_zfmisc_1(skc9,skc11)))
| ~ m1_subset_1(skc10,k1_zfmisc_1(k2_zfmisc_1(skc8,skc9)))
| ~ r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12))
| ~ equal(k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(rew,[status(thm),theory(equality)],[69,2026]),
[iquote('0:Rew:69.2,2026.3')] ).
cnf(2032,plain,
( ~ m1_subset_1(skc12,k1_zfmisc_1(k2_zfmisc_1(skc9,skc11)))
| ~ r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12))
| ~ equal(k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(mrr,[status(thm)],[2031,79]),
[iquote('0:MRR:2031.1,79.0')] ).
cnf(2033,plain,
( ~ r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12))
| ~ equal(k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(mrr,[status(thm)],[2032,83]),
[iquote('0:MRR:2032.0,83.0')] ).
cnf(2056,plain,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,skc9)))
| m2_relset_1(k5_relat_1(u,skc12),v,skc11) ),
inference(res,[status(thm),theory(equality)],[83,76]),
[iquote('0:Res:83.0,76.0')] ).
cnf(5187,plain,
m2_relset_1(k5_relat_1(skc10,skc12),skc8,skc11),
inference(res,[status(thm),theory(equality)],[79,2056]),
[iquote('0:Res:79.0,2056.0')] ).
cnf(5338,plain,
equal(k9_relat_1(k5_relat_1(skc10,skc12),skc8),k2_funct_5(k5_relat_1(skc10,skc12))),
inference(res,[status(thm),theory(equality)],[5187,513]),
[iquote('0:Res:5187.0,513.0')] ).
cnf(16488,plain,
( ~ v1_relat_1(skc10)
| ~ v1_relat_1(skc12)
| equal(k9_relat_1(skc12,k9_relat_1(skc10,skc8)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(spr,[status(thm),theory(equality)],[5338,67]),
[iquote('0:SpR:5338.0,67.2')] ).
cnf(16500,plain,
( ~ v1_relat_1(skc10)
| ~ v1_relat_1(skc12)
| equal(k9_relat_1(skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(rew,[status(thm),theory(equality)],[512,16488]),
[iquote('0:Rew:512.0,16488.2')] ).
cnf(16501,plain,
equal(k9_relat_1(skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))),
inference(ssi,[status(thm)],[16500,173,174]),
[iquote('0:SSi:16500.1,16500.0,173.0,174.0')] ).
cnf(16520,plain,
( ~ r1_tarski(k2_funct_5(skc10),skc9)
| r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12)) ),
inference(spr,[status(thm),theory(equality)],[16501,521]),
[iquote('0:SpR:16501.0,521.1')] ).
cnf(16528,plain,
r1_tarski(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(skc12)),
inference(mrr,[status(thm)],[16520,324]),
[iquote('0:MRR:16520.0,324.0')] ).
cnf(16529,plain,
~ equal(k10_relset_1(skc9,skc11,skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))),
inference(mrr,[status(thm)],[2033,16528]),
[iquote('0:MRR:2033.0,16528.0')] ).
cnf(16539,plain,
( ~ m1_relset_1(skc12,skc9,skc11)
| ~ equal(k9_relat_1(skc12,k2_funct_5(skc10)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(spl,[status(thm),theory(equality)],[64,16529]),
[iquote('0:SpL:64.1,16529.0')] ).
cnf(16540,plain,
( ~ m1_relset_1(skc12,skc9,skc11)
| ~ equal(k2_funct_5(k5_relat_1(skc10,skc12)),k2_funct_5(k5_relat_1(skc10,skc12))) ),
inference(rew,[status(thm),theory(equality)],[16501,16539]),
[iquote('0:Rew:16501.0,16539.1')] ).
cnf(16541,plain,
~ m1_relset_1(skc12,skc9,skc11),
inference(obv,[status(thm),theory(equality)],[16540]),
[iquote('0:Obv:16540.1')] ).
cnf(16542,plain,
$false,
inference(mrr,[status(thm)],[16541,84]),
[iquote('0:MRR:16541.0,84.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEU441+1 : TPTP v8.1.0. Released v3.4.0.
% 0.08/0.11 % Command : run_spass %d %s
% 0.08/0.31 % Computer : n027.cluster.edu
% 0.08/0.31 % Model : x86_64 x86_64
% 0.08/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.31 % Memory : 8042.1875MB
% 0.08/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.31 % CPULimit : 300
% 0.08/0.31 % WCLimit : 600
% 0.08/0.31 % DateTime : Sun Jun 19 01:26:08 EDT 2022
% 0.08/0.31 % CPUTime :
% 3.30/3.52
% 3.30/3.52 SPASS V 3.9
% 3.30/3.52 SPASS beiseite: Proof found.
% 3.30/3.52 % SZS status Theorem
% 3.30/3.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.30/3.52 SPASS derived 13740 clauses, backtracked 1565 clauses, performed 11 splits and kept 5510 clauses.
% 3.30/3.52 SPASS allocated 108775 KBytes.
% 3.30/3.52 SPASS spent 0:00:03.03 on the problem.
% 3.30/3.52 0:00:00.03 for the input.
% 3.30/3.52 0:00:00.03 for the FLOTTER CNF translation.
% 3.30/3.52 0:00:00.25 for inferences.
% 3.30/3.52 0:00:00.06 for the backtracking.
% 3.30/3.52 0:00:02.53 for the reduction.
% 3.30/3.52
% 3.30/3.52
% 3.30/3.52 Here is a proof with depth 6, length 55 :
% 3.30/3.52 % SZS output start Refutation
% See solution above
% 3.30/3.52 Formulae used in the proof : t53_relset_2 t21_funct_5 t3_subset cc1_relset_1 redefinition_m2_relset_1 dt_m2_relset_1 dt_k5_relset_1 redefinition_k5_relset_1 t51_relset_2 redefinition_k10_relset_1 t156_relat_1 t159_relat_1 dt_k9_relset_2 redefinition_k9_relset_2
% 3.30/3.52
%------------------------------------------------------------------------------