%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL088-1 : TPTP v9.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n002.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 : 300s
% DateTime : Wed Apr 9 05:48:00 PM UTC 2025
% Result : Unsatisfiable 27.05s 12.40s
% Output : CNFRefutation 27.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of formulae : 34 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 76 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 91 ( 49 ~; 42 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 41 ( 41 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ ap_contractE_c4 > ap_contractE_c3 > ap_contractE_c2 > ap_contractE_c1 > member > trans > ap_contractE_sk3q > ap_contractE_sk2q > ap_contractE_sk1q > ap_contractE_sk1p > pair > comb_app > #nlpp > rtrancl > z > y > r > p > contract > combS > combK > comb
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(r,type,
r: $i ).
tff(comb_app,type,
comb_app: ( $i * $i ) > $i ).
tff(ap_contractE_sk1q,type,
ap_contractE_sk1q: ( $i * $i * $i ) > $i ).
tff(trans,type,
trans: $i > $o ).
tff(ap_contractE_sk2q,type,
ap_contractE_sk2q: ( $i * $i * $i ) > $i ).
tff(rtrancl,type,
rtrancl: $i > $i ).
tff(ap_contractE_sk3q,type,
ap_contractE_sk3q: ( $i * $i * $i ) > $i ).
tff(y,type,
y: $i ).
tff(combS,type,
combS: $i ).
tff(member,type,
member: ( $i * $i ) > $o ).
tff(ap_contractE_c3,type,
ap_contractE_c3: ( $i * $i * $i ) > $o ).
tff(ap_contractE_c4,type,
ap_contractE_c4: ( $i * $i * $i ) > $o ).
tff(pair,type,
pair: ( $i * $i ) > $i ).
tff(contract,type,
contract: $i ).
tff(ap_contractE_c2,type,
ap_contractE_c2: ( $i * $i * $i ) > $o ).
tff(z,type,
z: $i ).
tff(combK,type,
combK: $i ).
tff(p,type,
p: $i ).
tff(ap_contractE_sk1p,type,
ap_contractE_sk1p: ( $i * $i * $i ) > $i ).
tff(comb,type,
comb: $i ).
tff(ap_contractE_c1,type,
ap_contractE_c1: ( $i * $i * $i ) > $o ).
tff(f_260,axiom,
member(pair(y,z),contract),
file(unknown,unknown) ).
tff(f_209,axiom,
! [A,B] :
( ~ member(pair(A,B),contract)
| member(B,comb) ),
file(unknown,unknown) ).
tff(f_257,axiom,
member(r,comb),
file(unknown,unknown) ).
tff(f_71,axiom,
! [P,Q] :
( ~ member(P,comb)
| ~ member(Q,comb)
| member(comb_app(P,Q),comb) ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [A] :
( ~ member(A,comb)
| member(pair(A,A),rtrancl(contract)) ),
file(unknown,unknown) ).
tff(f_245,axiom,
! [P3,Q3,R3,C] :
( ~ member(pair(P3,Q3),contract)
| ~ member(R3,comb)
| ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract))
| member(pair(comb_app(P3,R3),C),rtrancl(contract)) ),
file(unknown,unknown) ).
tff(f_263,axiom,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
file(unknown,unknown) ).
tff(f_261,axiom,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)),
file(unknown,unknown) ).
tff(f_204,axiom,
! [R] : trans(rtrancl(R)),
file(unknown,unknown) ).
tff(f_202,axiom,
! [R,A,B,C] :
( ~ trans(R)
| ~ member(pair(A,B),R)
| ~ member(pair(B,C),R)
| member(pair(A,C),R) ),
file(unknown,unknown) ).
tff(c_85,plain,
member(pair(y,z),contract),
inference(cnfTransformation,[status(thm)],[f_260]) ).
tff(c_106,plain,
! [B_127,A_128] :
( member(B_127,comb)
| ~ member(pair(A_128,B_127),contract) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_110,plain,
member(z,comb),
inference(resolution,[status(thm)],[c_85,c_106]) ).
tff(c_79,plain,
member(r,comb),
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_23,plain,
! [P_21,Q_22] :
( member(comb_app(P_21,Q_22),comb)
| ~ member(Q_22,comb)
| ~ member(P_21,comb) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_25,plain,
! [A_23] :
( member(pair(A_23,A_23),rtrancl(contract))
| ~ member(A_23,comb) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_535,plain,
! [P3_272,R3_273,C_274,Q3_275] :
( member(pair(comb_app(P3_272,R3_273),C_274),rtrancl(contract))
| ~ member(pair(comb_app(Q3_275,R3_273),C_274),rtrancl(contract))
| ~ member(R3_273,comb)
| ~ member(pair(P3_272,Q3_275),contract) ),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_1790,plain,
! [P3_686,R3_687,Q3_688] :
( member(pair(comb_app(P3_686,R3_687),comb_app(Q3_688,R3_687)),rtrancl(contract))
| ~ member(R3_687,comb)
| ~ member(pair(P3_686,Q3_688),contract)
| ~ member(comb_app(Q3_688,R3_687),comb) ),
inference(resolution,[status(thm)],[c_25,c_535]) ).
tff(c_89,plain,
~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)),
inference(cnfTransformation,[status(thm)],[f_263]) ).
tff(c_1802,plain,
( ~ member(r,comb)
| ~ member(pair(p,z),contract)
| ~ member(comb_app(z,r),comb) ),
inference(resolution,[status(thm)],[c_1790,c_89]) ).
tff(c_1853,plain,
( ~ member(pair(p,z),contract)
| ~ member(comb_app(z,r),comb) ),
inference(demodulation,[status(thm),theory(equality)],[c_79,c_1802]) ).
tff(c_1854,plain,
~ member(comb_app(z,r),comb),
inference(splitLeft,[status(thm)],[c_1853]) ).
tff(c_1857,plain,
( ~ member(r,comb)
| ~ member(z,comb) ),
inference(resolution,[status(thm)],[c_23,c_1854]) ).
tff(c_1861,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_110,c_79,c_1857]) ).
tff(c_1863,plain,
member(comb_app(z,r),comb),
inference(splitRight,[status(thm)],[c_1853]) ).
tff(c_87,plain,
member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_67,plain,
! [R_80] : trans(rtrancl(R_80)),
inference(cnfTransformation,[status(thm)],[f_204]) ).
tff(c_65,plain,
! [A_77,C_79,R_76,B_78] :
( member(pair(A_77,C_79),R_76)
| ~ member(pair(B_78,C_79),R_76)
| ~ member(pair(A_77,B_78),R_76)
| ~ trans(R_76) ),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_1799,plain,
! [A_77,Q3_688,R3_687,P3_686] :
( member(pair(A_77,comb_app(Q3_688,R3_687)),rtrancl(contract))
| ~ member(pair(A_77,comb_app(P3_686,R3_687)),rtrancl(contract))
| ~ trans(rtrancl(contract))
| ~ member(R3_687,comb)
| ~ member(pair(P3_686,Q3_688),contract)
| ~ member(comb_app(Q3_688,R3_687),comb) ),
inference(resolution,[status(thm)],[c_1790,c_65]) ).
tff(c_22723,plain,
! [A_2946,Q3_2947,R3_2948,P3_2949] :
( member(pair(A_2946,comb_app(Q3_2947,R3_2948)),rtrancl(contract))
| ~ member(pair(A_2946,comb_app(P3_2949,R3_2948)),rtrancl(contract))
| ~ member(R3_2948,comb)
| ~ member(pair(P3_2949,Q3_2947),contract)
| ~ member(comb_app(Q3_2947,R3_2948),comb) ),
inference(demodulation,[status(thm),theory(equality)],[c_67,c_1799]) ).
tff(c_22851,plain,
! [Q3_2947] :
( member(pair(comb_app(p,r),comb_app(Q3_2947,r)),rtrancl(contract))
| ~ member(r,comb)
| ~ member(pair(y,Q3_2947),contract)
| ~ member(comb_app(Q3_2947,r),comb) ),
inference(resolution,[status(thm)],[c_87,c_22723]) ).
tff(c_22907,plain,
! [Q3_2950] :
( member(pair(comb_app(p,r),comb_app(Q3_2950,r)),rtrancl(contract))
| ~ member(pair(y,Q3_2950),contract)
| ~ member(comb_app(Q3_2950,r),comb) ),
inference(demodulation,[status(thm),theory(equality)],[c_79,c_22851]) ).
tff(c_22952,plain,
( ~ member(pair(y,z),contract)
| ~ member(comb_app(z,r),comb) ),
inference(resolution,[status(thm)],[c_22907,c_89]) ).
tff(c_23024,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1863,c_85,c_22952]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : COL088-1 : TPTP v9.0.0. Released v2.7.0.
% 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n002.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 : 300
% 0.12/0.34 % DateTime : Mon Apr 7 16:02:01 EDT 2025
% 0.12/0.34 % CPUTime :
% 27.05/12.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.12/12.41
% 27.12/12.41 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------