%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COL088-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:02:01 PM UTC 2026
% Result : Unsatisfiable 138.15s 23.16s
% Output : Proof 138.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 16
% Syntax : Number of formulae : 111 ( 91 unt; 0 def)
% Number of atoms : 151 ( 65 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 106 ( 66 ~; 40 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-4 aty)
% Number of variables : 128 ( 22 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f31,axiom,
( member(pair(A,C),R)
| ~ member(pair(B,C),R)
| ~ member(pair(A,B),R)
| ~ trans(R) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transD) ).
fof(f31_nnf,plain,
! [R,A,B,C] :
( member(pair(A,C),R)
| ~ member(pair(B,C),R)
| ~ member(pair(A,B),R)
| ~ trans(R) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [R,A,B,C] :
( member(pair(A,C),R)
| ~ member(pair(B,C),R)
| ~ member(pair(A,B),R)
| ~ trans(R) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( member(pair(X1,X3),X0)
| ~ member(pair(X2,X3),X0)
| ~ member(pair(X1,X2),X0)
| ~ trans(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(t48,plain,
ifeq(trans(X1),true,ifeq(member(pair(X2,X3),X1),true,ifeq(member(pair(X3,X4),X1),true,member(pair(X2,X4),X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t198,plain,
ifeq(trans(X1),true,ifeq(member(pair(X2,X3),X1),true,ifeq(member(pair(X3,X4),X1),true,member(pair(X2,X4),X1),true),true),true) = true,
inference(orient,[status(thm)],[t48]) ).
cnf(f42,hypothesis,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_reduce1_2h5) ).
fof(f42_nnf,plain,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)),
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c42,plain,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)),
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(t31,plain,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)) = true,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(t63,plain,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)) = true,
inference(orient,[status(thm)],[t31]) ).
cnf(t200,plain,
true = ifeq(trans(rtrancl(contract)),true,ifeq(true,true,ifeq(member(pair(comb_app(y,r),X1),rtrancl(contract)),true,member(pair(comb_app(p,r),X1),rtrancl(contract)),true),true),true),
inference(cp,[status(thm)],[t198,t63]) ).
cnf(f32,axiom,
trans(rtrancl(R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_rtrancl) ).
fof(f32_nnf,plain,
! [R] : trans(rtrancl(R)),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [R] : trans(rtrancl(R)),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
trans(rtrancl(X0)),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t10,plain,
trans(rtrancl(X1)) = true,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t211,plain,
trans(rtrancl(X1)) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t309373,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(member(pair(comb_app(y,r),X1),rtrancl(contract)),true,member(pair(comb_app(p,r),X1),rtrancl(contract)),true),true),true),
inference(step,[status(thm)],[t200,t211]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t57,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t309374,plain,
true = ifeq(true,true,ifeq(member(pair(comb_app(y,r),X1),rtrancl(contract)),true,member(pair(comb_app(p,r),X1),rtrancl(contract)),true),true),
inference(step,[status(thm)],[t309373,t57]) ).
cnf(t309375,plain,
true = ifeq(member(pair(comb_app(y,r),X1),rtrancl(contract)),true,member(pair(comb_app(p,r),X1),rtrancl(contract)),true),
inference(step,[status(thm)],[t309374,t57]) ).
cnf(t306120,plain,
ifeq(member(pair(comb_app(y,r),X1),rtrancl(contract)),true,member(pair(comb_app(p,r),X1),rtrancl(contract)),true) = true,
inference(orient,[status(thm)],[t309375]) ).
cnf(f36,axiom,
( member(pair(comb_app(P3,R3),C),rtrancl(contract))
| ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(pair(P3,Q3),contract) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reduction_rls_3) ).
fof(f36_nnf,plain,
! [P3,Q3,R3,C] :
( member(pair(comb_app(P3,R3),C),rtrancl(contract))
| ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(pair(P3,Q3),contract) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [P3,Q3,R3,C] :
( member(pair(comb_app(P3,R3),C),rtrancl(contract))
| ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract))
| ~ member(R3,comb)
| ~ member(pair(P3,Q3),contract) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
( member(pair(comb_app(X0,X2),X3),rtrancl(contract))
| ~ member(pair(comb_app(X1,X2),X3),rtrancl(contract))
| ~ member(X2,comb)
| ~ member(pair(X0,X1),contract) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(t53,plain,
ifeq(member(pair(X1,X2),contract),true,ifeq(member(X3,comb),true,ifeq(member(pair(comb_app(X2,X3),X4),rtrancl(contract)),true,member(pair(comb_app(X1,X3),X4),rtrancl(contract)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t154,plain,
ifeq(member(pair(X1,X2),contract),true,ifeq(member(X3,comb),true,ifeq(member(pair(comb_app(X2,X3),X4),rtrancl(contract)),true,member(pair(comb_app(X1,X3),X4),rtrancl(contract)),true),true),true) = true,
inference(orient,[status(thm)],[t53]) ).
cnf(f41,hypothesis,
member(pair(y,z),contract),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_reduce1_2h4) ).
fof(f41_nnf,plain,
member(pair(y,z),contract),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
member(pair(y,z),contract),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(t17,plain,
member(pair(y,z),contract) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t65,plain,
member(pair(y,z),contract) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t155,plain,
true = ifeq(true,true,ifeq(member(X1,comb),true,ifeq(member(pair(comb_app(z,X1),X2),rtrancl(contract)),true,member(pair(comb_app(y,X1),X2),rtrancl(contract)),true),true),true),
inference(cp,[status(thm)],[t154,t65]) ).
cnf(t308986,plain,
true = ifeq(member(X1,comb),true,ifeq(member(pair(comb_app(z,X1),X2),rtrancl(contract)),true,member(pair(comb_app(y,X1),X2),rtrancl(contract)),true),true),
inference(step,[status(thm)],[t155,t57]) ).
cnf(t268163,plain,
ifeq(member(X1,comb),true,ifeq(member(pair(comb_app(z,X1),X2),rtrancl(contract)),true,member(pair(comb_app(y,X1),X2),rtrancl(contract)),true),true) = true,
inference(orient,[status(thm)],[t308986]) ).
cnf(f11,axiom,
( member(pair(A,A),rtrancl(contract))
| ~ member(A,comb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reduction_refl) ).
fof(f11_nnf,plain,
! [A] :
( member(pair(A,A),rtrancl(contract))
| ~ member(A,comb) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A] :
( member(pair(A,A),rtrancl(contract))
| ~ member(A,comb) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( member(pair(X0,X0),rtrancl(contract))
| ~ member(X0,comb) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t37,plain,
ifeq(member(X1,comb),true,member(pair(X1,X1),rtrancl(contract)),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t70,plain,
ifeq(member(X1,comb),true,member(pair(X1,X1),rtrancl(contract)),true) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(f10,axiom,
( member(comb_app(P,Q),comb)
| ~ member(Q,comb)
| ~ member(P,comb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',comb_intros3) ).
fof(f10_nnf,plain,
! [P,Q] :
( member(comb_app(P,Q),comb)
| ~ member(Q,comb)
| ~ member(P,comb) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [P,Q] :
( member(comb_app(P,Q),comb)
| ~ member(Q,comb)
| ~ member(P,comb) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( member(comb_app(X0,X1),comb)
| ~ member(X1,comb)
| ~ member(X0,comb) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t44,plain,
ifeq(member(X1,comb),true,ifeq(member(X2,comb),true,member(comb_app(X1,X2),comb),true),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t75,plain,
ifeq(member(X1,comb),true,ifeq(member(X2,comb),true,member(comb_app(X1,X2),comb),true),true) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(f38,hypothesis,
member(r,comb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_reduce1_2h1) ).
fof(f38_nnf,plain,
member(r,comb),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
member(r,comb),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
cnf(t5,plain,
member(r,comb) = true,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t68,plain,
member(r,comb) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t81,plain,
true = ifeq(member(X1,comb),true,ifeq(true,true,member(comb_app(X1,r),comb),true),true),
inference(cp,[status(thm)],[t75,t68]) ).
cnf(t306385,plain,
true = ifeq(member(X1,comb),true,member(comb_app(X1,r),comb),true),
inference(step,[status(thm)],[t81,t57]) ).
cnf(t6670,plain,
ifeq(member(X1,comb),true,member(comb_app(X1,r),comb),true) = true,
inference(orient,[status(thm)],[t306385]) ).
cnf(f33,axiom,
( member(B,comb)
| ~ member(pair(A,B),contract) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',contract_combD2) ).
fof(f33_nnf,plain,
! [A,B] :
( member(B,comb)
| ~ member(pair(A,B),contract) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [A,B] :
( member(B,comb)
| ~ member(pair(A,B),contract) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
( member(X1,comb)
| ~ member(pair(X0,X1),contract) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t35,plain,
ifeq(member(pair(X1,X2),contract),true,member(X2,comb),true) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t140,plain,
ifeq(member(pair(X1,X2),contract),true,member(X2,comb),true) = true,
inference(orient,[status(thm)],[t35]) ).
cnf(t141,plain,
true = ifeq(true,true,member(z,comb),true),
inference(cp,[status(thm)],[t140,t65]) ).
cnf(t306156,plain,
true = member(z,comb),
inference(step,[status(thm)],[t141,t57]) ).
cnf(t257,plain,
member(z,comb) = true,
inference(orient,[status(thm)],[t306156]) ).
cnf(t6886,plain,
true = ifeq(true,true,member(comb_app(z,r),comb),true),
inference(cp,[status(thm)],[t6670,t257]) ).
cnf(t306386,plain,
true = member(comb_app(z,r),comb),
inference(step,[status(thm)],[t6886,t57]) ).
cnf(t6887,plain,
member(comb_app(z,r),comb) = true,
inference(orient,[status(thm)],[t306386]) ).
cnf(t6902,plain,
true = ifeq(true,true,member(pair(comb_app(z,r),comb_app(z,r)),rtrancl(contract)),true),
inference(cp,[status(thm)],[t70,t6887]) ).
cnf(t307998,plain,
true = member(pair(comb_app(z,r),comb_app(z,r)),rtrancl(contract)),
inference(step,[status(thm)],[t6902,t57]) ).
cnf(t151835,plain,
member(pair(comb_app(z,r),comb_app(z,r)),rtrancl(contract)) = true,
inference(orient,[status(thm)],[t307998]) ).
cnf(t270809,plain,
true = ifeq(member(r,comb),true,ifeq(true,true,member(pair(comb_app(y,r),comb_app(z,r)),rtrancl(contract)),true),true),
inference(cp,[status(thm)],[t268163,t151835]) ).
cnf(t309159,plain,
true = ifeq(true,true,ifeq(true,true,member(pair(comb_app(y,r),comb_app(z,r)),rtrancl(contract)),true),true),
inference(step,[status(thm)],[t270809,t68]) ).
cnf(t309160,plain,
true = ifeq(true,true,member(pair(comb_app(y,r),comb_app(z,r)),rtrancl(contract)),true),
inference(step,[status(thm)],[t309159,t57]) ).
cnf(t309161,plain,
true = member(pair(comb_app(y,r),comb_app(z,r)),rtrancl(contract)),
inference(step,[status(thm)],[t309160,t57]) ).
cnf(t285290,plain,
member(pair(comb_app(y,r),comb_app(z,r)),rtrancl(contract)) = true,
inference(orient,[status(thm)],[t309161]) ).
cnf(t306121,plain,
true = ifeq(true,true,member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),true),
inference(cp,[status(thm)],[t306120,t285290]) ).
cnf(t309376,plain,
true = member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
inference(step,[status(thm)],[t306121,t57]) ).
cnf(f43,negated_conjecture,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ap_reduce1_2c1) ).
fof(f43_nnf,plain,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(t32,plain,
member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)) = false,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t213,plain,
member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)) = false,
inference(orient,[status(thm)],[t32]) ).
cnf(t309377,plain,
true = false,
inference(step,[status(thm)],[t309376,t213]) ).
cnf(t306127,plain,
false = true,
inference(orient,[status(thm)],[t309377]) ).
cnf(f0,axiom,
combK != combS,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_s) ).
fof(f0_nnf,plain,
combK != combS,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
combK != combS,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
combK != combS,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f1,axiom,
combK != comb_app(P,Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_app) ).
fof(f1_nnf,plain,
! [P,Q] : combK != comb_app(P,Q),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [P,Q] : combK != comb_app(P,Q),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
combK != comb_app(X0,X1),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f2,axiom,
combS != comb_app(P,Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s_app) ).
fof(f2_nnf,plain,
! [P,Q] : combS != comb_app(P,Q),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [P,Q] : combS != comb_app(P,Q),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
combS != comb_app(X0,X1),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f29,axiom,
~ member(pair(combK,R),contract),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_contractE) ).
fof(f29_nnf,plain,
! [R] : ~ member(pair(combK,R),contract),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [R] : ~ member(pair(combK,R),contract),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
~ member(pair(combK,X0),contract),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f30,axiom,
~ member(pair(combS,R),contract),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s_contractE) ).
fof(f30_nnf,plain,
! [R] : ~ member(pair(combS,R),contract),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [R] : ~ member(pair(combS,R),contract),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
~ member(pair(combS,X0),contract),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c2,c29,c30,c43]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t306127]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL088-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n008.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Fri Sep 25 07:32:29 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 138.15/23.16 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 138.15/23.16 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------