%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : COL090-3 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.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 : Fri Jul 15 00:42:37 EDT 2022
% Result : Unsatisfiable 1.59s 1.75s
% Output : Refutation 1.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 16
% Syntax : Number of clauses : 59 ( 22 unt; 8 nHn; 59 RR)
% Number of literals : 117 ( 0 equ; 60 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ equal(combS,combK),
file('COL090-3.p',unknown),
[] ).
cnf(2,axiom,
~ equal(comb_app(u,v),combK),
file('COL090-3.p',unknown),
[] ).
cnf(3,axiom,
~ equal(comb_app(u,v),combS),
file('COL090-3.p',unknown),
[] ).
cnf(4,axiom,
( ~ equal(comb_app(u,v),comb_app(w,x))
| equal(u,w) ),
file('COL090-3.p',unknown),
[] ).
cnf(5,axiom,
( ~ equal(comb_app(u,v),comb_app(w,x))
| equal(v,x) ),
file('COL090-3.p',unknown),
[] ).
cnf(6,axiom,
( ~ equal(u,v)
| ~ equal(w,x)
| equal(comb_app(w,u),comb_app(x,v)) ),
file('COL090-3.p',unknown),
[] ).
cnf(7,axiom,
( ~ member(pair(comb_app(u,v),w),contract)
| ap_contractE_c4(u,v,w)
| ap_contractE_c3(u,v,w)
| ap_contractE_c2(u,v,w)
| ap_contractE_c1(u,v,w) ),
file('COL090-3.p',unknown),
[] ).
cnf(10,axiom,
( ~ ap_contractE_c1(u,v,w)
| equal(u,comb_app(combK,w)) ),
file('COL090-3.p',unknown),
[] ).
cnf(14,axiom,
( ~ ap_contractE_c2(u,v,w)
| equal(comb_app(comb_app(ap_contractE_sk1p(u,v,w),v),comb_app(ap_contractE_sk1q(u,v,w),v)),w) ),
file('COL090-3.p',unknown),
[] ).
cnf(15,axiom,
( ~ ap_contractE_c2(u,v,w)
| equal(comb_app(comb_app(combS,ap_contractE_sk1p(u,v,w)),ap_contractE_sk1q(u,v,w)),u) ),
file('COL090-3.p',unknown),
[] ).
cnf(16,axiom,
( ~ ap_contractE_c3(u,v,w)
| member(pair(u,ap_contractE_sk2q(u,v,w)),contract) ),
file('COL090-3.p',unknown),
[] ).
cnf(18,axiom,
( ~ ap_contractE_c3(u,v,w)
| equal(comb_app(ap_contractE_sk2q(u,v,w),v),w) ),
file('COL090-3.p',unknown),
[] ).
cnf(19,axiom,
( ~ ap_contractE_c4(u,v,w)
| member(pair(v,ap_contractE_sk3q(u,v,w)),contract) ),
file('COL090-3.p',unknown),
[] ).
cnf(22,axiom,
~ member(pair(combK,u),contract),
file('COL090-3.p',unknown),
[] ).
cnf(23,axiom,
~ member(pair(combS,u),contract),
file('COL090-3.p',unknown),
[] ).
cnf(24,axiom,
member(pair(comb_app(comb_app(combS,combK),combK),r),contract),
file('COL090-3.p',unknown),
[] ).
cnf(25,plain,
( ap_contractE_c4(comb_app(combS,combK),combK,r)
| ap_contractE_c3(comb_app(combS,combK),combK,r)
| ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c1(comb_app(combS,combK),combK,r) ),
inference(res,[status(thm),theory(equality)],[24,7]),
[iquote('0:Res:24.0,7.0')] ).
cnf(29,plain,
~ ap_contractE_c4(u,combK,v),
inference(res,[status(thm),theory(equality)],[19,22]),
[iquote('0:Res:19.1,22.0')] ).
cnf(30,plain,
( ap_contractE_c3(comb_app(combS,combK),combK,r)
| ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c1(comb_app(combS,combK),combK,r) ),
inference(mrr,[status(thm)],[25,29]),
[iquote('0:MRR:25.0,29.0')] ).
cnf(31,plain,
~ ap_contractE_c3(combS,u,v),
inference(res,[status(thm),theory(equality)],[16,23]),
[iquote('0:Res:16.1,23.0')] ).
cnf(36,plain,
( ~ ap_contractE_c3(u,v,w)
| ~ equal(w,comb_app(x,y))
| equal(ap_contractE_sk2q(u,v,w),x) ),
inference(spl,[status(thm),theory(equality)],[18,4]),
[iquote('0:SpL:18.1,4.0')] ).
cnf(114,plain,
( ~ ap_contractE_c2(u,v,w)
| ~ equal(u,combS) ),
inference(spl,[status(thm),theory(equality)],[15,3]),
[iquote('0:SpL:15.1,3.0')] ).
cnf(116,plain,
( ~ ap_contractE_c2(u,v,w)
| ~ equal(u,comb_app(x,y))
| equal(comb_app(combS,ap_contractE_sk1p(u,v,w)),x) ),
inference(spl,[status(thm),theory(equality)],[15,4]),
[iquote('0:SpL:15.1,4.0')] ).
cnf(141,plain,
( ~ ap_contractE_c2(u,v,w)
| ~ equal(w,comb_app(x,y))
| equal(comb_app(ap_contractE_sk1q(u,v,w),v),y) ),
inference(spl,[status(thm),theory(equality)],[14,5]),
[iquote('0:SpL:14.1,5.0')] ).
cnf(217,plain,
( ~ ap_contractE_c3(u,v,comb_app(w,x))
| equal(ap_contractE_sk2q(u,v,comb_app(w,x)),w) ),
inference(eqr,[status(thm),theory(equality)],[36]),
[iquote('0:EqR:36.1')] ).
cnf(226,plain,
( ~ ap_contractE_c3(u,v,comb_app(w,x))
| ~ ap_contractE_c3(u,v,comb_app(w,x))
| member(pair(u,w),contract) ),
inference(spr,[status(thm),theory(equality)],[217,16]),
[iquote('0:SpR:217.1,16.1')] ).
cnf(235,plain,
( ~ ap_contractE_c3(u,v,comb_app(w,x))
| member(pair(u,w),contract) ),
inference(obv,[status(thm),theory(equality)],[226]),
[iquote('0:Obv:226.0')] ).
cnf(241,plain,
( ~ ap_contractE_c3(u,v,w)
| ~ ap_contractE_c3(x,y,w)
| member(pair(x,ap_contractE_sk2q(u,v,w)),contract) ),
inference(spl,[status(thm),theory(equality)],[18,235]),
[iquote('0:SpL:18.1,235.0')] ).
cnf(350,plain,
( ~ ap_contractE_c2(comb_app(u,v),w,x)
| equal(comb_app(combS,ap_contractE_sk1p(comb_app(u,v),w,x)),u) ),
inference(eqr,[status(thm),theory(equality)],[116]),
[iquote('0:EqR:116.1')] ).
cnf(492,plain,
( ~ ap_contractE_c2(u,v,comb_app(w,x))
| equal(comb_app(ap_contractE_sk1q(u,v,comb_app(w,x)),v),x) ),
inference(eqr,[status(thm),theory(equality)],[141]),
[iquote('0:EqR:141.1')] ).
cnf(683,plain,
( ~ ap_contractE_c2(comb_app(u,v),w,x)
| ~ equal(u,combS) ),
inference(spl,[status(thm),theory(equality)],[350,3]),
[iquote('0:SpL:350.1,3.0')] ).
cnf(736,plain,
( ~ equal(u,v)
| ~ equal(w,x)
| ~ ap_contractE_c2(comb_app(w,u),y,z)
| ~ equal(x,combS) ),
inference(spl,[status(thm),theory(equality)],[6,683]),
[iquote('0:SpL:6.2,683.0')] ).
cnf(744,plain,
( ~ equal(u,v)
| ~ ap_contractE_c2(comb_app(u,w),x,y)
| ~ equal(v,combS) ),
inference(aed,[status(thm),theory(equality)],[1,736]),
[iquote('0:AED:1.0,736.0')] ).
cnf(1516,plain,
( ~ ap_contractE_c2(u,v,comb_app(w,x))
| ~ equal(x,combK) ),
inference(spl,[status(thm),theory(equality)],[492,2]),
[iquote('0:SpL:492.1,2.0')] ).
cnf(1641,plain,
( ~ ap_contractE_c3(u,v,w)
| ~ ap_contractE_c2(x,y,w)
| ~ equal(v,combK) ),
inference(spl,[status(thm),theory(equality)],[18,1516]),
[iquote('0:SpL:18.1,1516.0')] ).
cnf(1661,plain,
( ~ ap_contractE_c2(u,v,r)
| ~ equal(combK,combK)
| ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c1(comb_app(combS,combK),combK,r) ),
inference(res,[status(thm),theory(equality)],[30,1641]),
[iquote('0:Res:30.0,1641.0')] ).
cnf(1662,plain,
( ~ ap_contractE_c2(u,v,r)
| ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c1(comb_app(combS,combK),combK,r) ),
inference(obv,[status(thm),theory(equality)],[1661]),
[iquote('0:Obv:1661.1')] ).
cnf(2122,plain,
ap_contractE_c1(comb_app(combS,combK),combK,r),
inference(spt,[spt(split,[position(s1)])],[1662]),
[iquote('1:Spt:1662.2')] ).
cnf(2125,plain,
equal(comb_app(combS,combK),comb_app(combK,r)),
inference(res,[status(thm),theory(equality)],[2122,10]),
[iquote('1:Res:2122.0,10.0')] ).
cnf(2170,plain,
( ~ equal(comb_app(combK,r),comb_app(u,v))
| equal(combS,u) ),
inference(spl,[status(thm),theory(equality)],[2125,4]),
[iquote('1:SpL:2125.0,4.0')] ).
cnf(2291,plain,
equal(combS,combK),
inference(eqr,[status(thm),theory(equality)],[2170]),
[iquote('1:EqR:2170.0')] ).
cnf(2309,plain,
$false,
inference(mrr,[status(thm)],[2291,1]),
[iquote('1:MRR:2291.0,1.0')] ).
cnf(2314,plain,
~ ap_contractE_c1(comb_app(combS,combK),combK,r),
inference(spt,[spt(split,[position(sa)])],[2309,2122]),
[iquote('1:Spt:2309.0,1662.2,2122.0')] ).
cnf(2315,plain,
( ~ ap_contractE_c2(u,v,r)
| ap_contractE_c2(comb_app(combS,combK),combK,r) ),
inference(spt,[spt(split,[position(s2)])],[1662]),
[iquote('1:Spt:2309.0,1662.0,1662.1')] ).
cnf(2316,plain,
( ap_contractE_c3(comb_app(combS,combK),combK,r)
| ap_contractE_c2(comb_app(combS,combK),combK,r) ),
inference(mrr,[status(thm)],[30,2314]),
[iquote('1:MRR:30.2,2314.0')] ).
cnf(2333,plain,
ap_contractE_c2(comb_app(combS,combK),combK,r),
inference(spt,[spt(split,[position(s2s1)])],[2316]),
[iquote('2:Spt:2316.1')] ).
cnf(2355,plain,
( ~ equal(combS,u)
| ~ equal(u,combS) ),
inference(res,[status(thm),theory(equality)],[2333,744]),
[iquote('2:Res:2333.0,744.1')] ).
cnf(2360,plain,
~ equal(u,combS),
inference(obv,[status(thm),theory(equality)],[2355]),
[iquote('2:Obv:2355.0')] ).
cnf(2361,plain,
$false,
inference(aed,[status(thm),theory(equality)],[1,2360]),
[iquote('2:AED:1.0,2360.0')] ).
cnf(2364,plain,
~ ap_contractE_c2(comb_app(combS,combK),combK,r),
inference(spt,[spt(split,[position(s2sa)])],[2361,2333]),
[iquote('2:Spt:2361.0,2316.1,2333.0')] ).
cnf(2365,plain,
ap_contractE_c3(comb_app(combS,combK),combK,r),
inference(spt,[spt(split,[position(s2s2)])],[2316]),
[iquote('2:Spt:2361.0,2316.0')] ).
cnf(3006,plain,
( ~ ap_contractE_c3(u,v,r)
| member(pair(u,ap_contractE_sk2q(comb_app(combS,combK),combK,r)),contract) ),
inference(res,[status(thm),theory(equality)],[2365,241]),
[iquote('2:Res:2365.0,241.0')] ).
cnf(3047,plain,
member(pair(comb_app(combS,combK),ap_contractE_sk2q(comb_app(combS,combK),combK,r)),contract),
inference(res,[status(thm),theory(equality)],[2365,3006]),
[iquote('2:Res:2365.0,3006.0')] ).
cnf(3053,plain,
( ap_contractE_c4(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r))
| ap_contractE_c3(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r))
| ap_contractE_c2(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r))
| ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r)) ),
inference(res,[status(thm),theory(equality)],[3047,7]),
[iquote('2:Res:3047.0,7.0')] ).
cnf(3055,plain,
( ap_contractE_c2(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r))
| ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r)) ),
inference(mrr,[status(thm)],[3053,29,31]),
[iquote('2:MRR:3053.0,3053.1,29.0,31.0')] ).
cnf(3064,plain,
( ~ equal(combS,combS)
| ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r)) ),
inference(res,[status(thm),theory(equality)],[3055,114]),
[iquote('2:Res:3055.0,114.0')] ).
cnf(3066,plain,
ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r)),
inference(obv,[status(thm),theory(equality)],[3064]),
[iquote('2:Obv:3064.0')] ).
cnf(3069,plain,
equal(comb_app(combK,ap_contractE_sk2q(comb_app(combS,combK),combK,r)),combS),
inference(res,[status(thm),theory(equality)],[3066,10]),
[iquote('2:Res:3066.0,10.0')] ).
cnf(3072,plain,
$false,
inference(mrr,[status(thm)],[3069,3]),
[iquote('2:MRR:3069.0,3.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : COL090-3 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Tue May 31 07:07:40 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.59/1.75
% 1.59/1.75 SPASS V 3.9
% 1.59/1.75 SPASS beiseite: Proof found.
% 1.59/1.75 % SZS status Theorem
% 1.59/1.75 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.59/1.75 SPASS derived 2252 clauses, backtracked 50 clauses, performed 2 splits and kept 1352 clauses.
% 1.59/1.75 SPASS allocated 66639 KBytes.
% 1.59/1.75 SPASS spent 0:00:01.38 on the problem.
% 1.59/1.75 0:00:00.04 for the input.
% 1.59/1.75 0:00:00.00 for the FLOTTER CNF translation.
% 1.59/1.75 0:00:00.05 for inferences.
% 1.59/1.75 0:00:00.00 for the backtracking.
% 1.59/1.75 0:00:01.26 for the reduction.
% 1.59/1.75
% 1.59/1.75
% 1.59/1.75 Here is a proof with depth 9, length 59 :
% 1.59/1.75 % SZS output start Refutation
% See solution above
% 1.59/1.75 Formulae used in the proof : k_s k_app s_app app_app1 app_app2 app_app3 ap_contractE1 ap_contractE4 ap_contractE8 ap_contractE9 ap_contractE10 ap_contractE12 ap_contractE13 k_contractE s_contractE i_contract_E
% 1.59/1.75
%------------------------------------------------------------------------------