%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : COL088-1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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:36 EDT 2022
% Result : Unsatisfiable 25.94s 26.19s
% Output : Refutation 25.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of clauses : 21 ( 8 unt; 0 nHn; 21 RR)
% Number of literals : 44 ( 0 equ; 30 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(8,axiom,
( ~ member(comb_app(u,v),comb)
| member(v,comb) ),
file('COL088-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ member(u,comb)
| ~ member(v,comb)
| member(comb_app(v,u),comb) ),
file('COL088-1.p',unknown),
[] ).
cnf(12,axiom,
( ~ member(u,comb)
| member(pair(u,u),rtrancl(contract)) ),
file('COL088-1.p',unknown),
[] ).
cnf(32,axiom,
( ~ trans(u)
| ~ member(pair(v,w),u)
| ~ member(pair(x,v),u)
| member(pair(x,w),u) ),
file('COL088-1.p',unknown),
[] ).
cnf(33,axiom,
trans(rtrancl(u)),
file('COL088-1.p',unknown),
[] ).
cnf(34,axiom,
( ~ member(pair(u,v),contract)
| member(v,comb) ),
file('COL088-1.p',unknown),
[] ).
cnf(37,axiom,
( ~ member(u,comb)
| ~ member(pair(v,w),contract)
| ~ member(pair(comb_app(w,u),x),rtrancl(contract))
| member(pair(comb_app(v,u),x),rtrancl(contract)) ),
file('COL088-1.p',unknown),
[] ).
cnf(39,axiom,
member(r,comb),
file('COL088-1.p',unknown),
[] ).
cnf(42,axiom,
member(pair(y__dfg,z__dfg),contract),
file('COL088-1.p',unknown),
[] ).
cnf(43,axiom,
member(pair(comb_app(p,r),comb_app(y__dfg,r)),rtrancl(contract)),
file('COL088-1.p',unknown),
[] ).
cnf(44,axiom,
~ member(pair(comb_app(p,r),comb_app(z__dfg,r)),rtrancl(contract)),
file('COL088-1.p',unknown),
[] ).
cnf(47,plain,
( ~ trans(rtrancl(contract))
| ~ member(pair(comb_app(p,r),u),rtrancl(contract))
| ~ member(pair(u,comb_app(z__dfg,r)),rtrancl(contract)) ),
inference(res,[status(thm),theory(equality)],[32,44]),
[iquote('0:Res:32.3,44.0')] ).
cnf(50,plain,
( ~ member(pair(u,comb_app(z__dfg,r)),rtrancl(contract))
| ~ member(pair(comb_app(p,r),u),rtrancl(contract)) ),
inference(mrr,[status(thm)],[47,33]),
[iquote('0:MRR:47.0,33.0')] ).
cnf(51,plain,
member(z__dfg,comb),
inference(res,[status(thm),theory(equality)],[42,34]),
[iquote('0:Res:42.0,34.0')] ).
cnf(374,plain,
( ~ member(comb_app(u,v),comb)
| ~ member(v,comb)
| ~ member(pair(w,u),contract)
| member(pair(comb_app(w,v),comb_app(u,v)),rtrancl(contract)) ),
inference(res,[status(thm),theory(equality)],[12,37]),
[iquote('0:Res:12.1,37.2')] ).
cnf(378,plain,
( ~ member(comb_app(u,v),comb)
| ~ member(pair(w,u),contract)
| member(pair(comb_app(w,v),comb_app(u,v)),rtrancl(contract)) ),
inference(mrr,[status(thm)],[374,8]),
[iquote('0:MRR:374.1,8.1')] ).
cnf(1577,plain,
( ~ member(comb_app(z__dfg,r),comb)
| ~ member(pair(u,z__dfg),contract)
| ~ member(pair(comb_app(p,r),comb_app(u,r)),rtrancl(contract)) ),
inference(res,[status(thm),theory(equality)],[378,50]),
[iquote('0:Res:378.2,50.0')] ).
cnf(15018,plain,
( ~ member(comb_app(z__dfg,r),comb)
| ~ member(pair(y__dfg,z__dfg),contract) ),
inference(res,[status(thm),theory(equality)],[43,1577]),
[iquote('0:Res:43.0,1577.2')] ).
cnf(15037,plain,
~ member(comb_app(z__dfg,r),comb),
inference(mrr,[status(thm)],[15018,42]),
[iquote('0:MRR:15018.1,42.0')] ).
cnf(15047,plain,
( ~ member(r,comb)
| ~ member(z__dfg,comb) ),
inference(res,[status(thm),theory(equality)],[11,15037]),
[iquote('0:Res:11.2,15037.0')] ).
cnf(15048,plain,
$false,
inference(mrr,[status(thm)],[15047,39,51]),
[iquote('0:MRR:15047.0,15047.1,39.0,51.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : COL088-1 : TPTP v8.1.0. Released v2.7.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n025.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 13:47:28 EDT 2022
% 0.13/0.34 % CPUTime :
% 25.94/26.19
% 25.94/26.19 SPASS V 3.9
% 25.94/26.19 SPASS beiseite: Proof found.
% 25.94/26.19 % SZS status Theorem
% 25.94/26.19 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.94/26.19 SPASS derived 10628 clauses, backtracked 0 clauses, performed 0 splits and kept 6929 clauses.
% 25.94/26.19 SPASS allocated 97282 KBytes.
% 25.94/26.19 SPASS spent 0:0:25.51 on the problem.
% 25.94/26.19 0:00:00.04 for the input.
% 25.94/26.19 0:00:00.00 for the FLOTTER CNF translation.
% 25.94/26.19 0:00:00.36 for inferences.
% 25.94/26.19 0:00:00.00 for the backtracking.
% 25.94/26.19 0:0:24.96 for the reduction.
% 25.94/26.19
% 25.94/26.19
% 25.94/26.19 Here is a proof with depth 4, length 21 :
% 25.94/26.19 % SZS output start Refutation
% See solution above
% 25.94/26.19 Formulae used in the proof : ap_E2 comb_intros3 reduction_refl transD trans_rtrancl contract_combD2 reduction_rls_3 ap_reduce1_2h1 ap_reduce1_2h4 ap_reduce1_2h5 ap_reduce1_2c1
% 25.94/26.19
%------------------------------------------------------------------------------