%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL090-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 : n029.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:01 PM UTC 2025
% Result : Unsatisfiable 14.51s 4.93s
% Output : CNFRefutation 14.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 52 ( 24 unt; 0 typ; 0 def)
% Number of atoms : 96 ( 29 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 83 ( 39 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 96 ( 96 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ ap_contractE_c4 > ap_contractE_c3 > ap_contractE_c2 > ap_contractE_c1 > member > ap_contractE_sk3q > ap_contractE_sk2q > ap_contractE_sk1q > ap_contractE_sk1p > pair > comb_app > #nlpp > rtrancl > r > 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(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(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(combK,type,
combK: $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_150,axiom,
! [P,Q,R] :
( ~ ap_contractE_c2(P,Q,R)
| ( P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R)) ) ),
file(unknown,unknown) ).
tff(f_36,axiom,
! [P1,Q1,P2,Q2] :
( ( comb_app(P1,Q1) != comb_app(P2,Q2) )
| ( P1 = P2 ) ),
file(unknown,unknown) ).
tff(f_31,axiom,
! [P,Q] : ( combS != comb_app(P,Q) ),
file(unknown,unknown) ).
tff(f_155,axiom,
! [P,Q,R] :
( ~ ap_contractE_c3(P,Q,R)
| member(pair(P,ap_contractE_sk2q(P,Q,R)),contract) ),
file(unknown,unknown) ).
tff(f_110,axiom,
! [P,Q,R] :
( ~ member(pair(comb_app(P,Q),R),contract)
| ap_contractE_c1(P,Q,R)
| ap_contractE_c2(P,Q,R)
| ap_contractE_c3(P,Q,R)
| ap_contractE_c4(P,Q,R) ),
file(unknown,unknown) ).
tff(f_170,axiom,
! [P,Q,R] :
( ~ ap_contractE_c4(P,Q,R)
| member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract) ),
file(unknown,unknown) ).
tff(f_184,axiom,
! [R] : ~ member(pair(combK,R),contract),
file(unknown,unknown) ).
tff(f_189,axiom,
! [R] : ~ member(pair(combS,R),contract),
file(unknown,unknown) ).
tff(f_125,axiom,
! [P,Q,R] :
( ~ ap_contractE_c1(P,Q,R)
| ( P = comb_app(combK,R) ) ),
file(unknown,unknown) ).
tff(f_25,axiom,
combK != combS,
file(unknown,unknown) ).
tff(f_190,axiom,
member(pair(comb_app(comb_app(combS,combK),combK),r),contract),
file(unknown,unknown) ).
tff(f_41,axiom,
! [P1,Q1,P2,Q2] :
( ( comb_app(P1,Q1) != comb_app(P2,Q2) )
| ( Q1 = Q2 ) ),
file(unknown,unknown) ).
tff(c_272,plain,
! [P_196,Q_197,R_198] :
( ( comb_app(comb_app(combS,ap_contractE_sk1p(P_196,Q_197,R_198)),ap_contractE_sk1q(P_196,Q_197,R_198)) = P_196 )
| ~ ap_contractE_c2(P_196,Q_197,R_198) ),
inference(cnfTransformation,[status(thm)],[f_150]) ).
tff(c_8,plain,
! [P2_7,P1_5,Q2_8,Q1_6] :
( ( P2_7 = P1_5 )
| ( comb_app(P2_7,Q2_8) != comb_app(P1_5,Q1_6) ) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_298,plain,
! [Q_197,R_198,P2_7,P_196,Q2_8] :
( ( comb_app(combS,ap_contractE_sk1p(P_196,Q_197,R_198)) = P2_7 )
| ( comb_app(P2_7,Q2_8) != P_196 )
| ~ ap_contractE_c2(P_196,Q_197,R_198) ),
inference(superposition,[status(thm),theory(equality)],[c_272,c_8]) ).
tff(c_13892,plain,
! [P2_2449,Q2_2450,Q_2451,R_2452] :
( ( comb_app(combS,ap_contractE_sk1p(comb_app(P2_2449,Q2_2450),Q_2451,R_2452)) = P2_2449 )
| ~ ap_contractE_c2(comb_app(P2_2449,Q2_2450),Q_2451,R_2452) ),
inference(reflexivity,[status(thm),theory(equality)],[c_298]) ).
tff(c_6,plain,
! [P_3,Q_4] : ( comb_app(P_3,Q_4) != combS ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_14173,plain,
! [Q2_2450,Q_2451,R_2452] : ~ ap_contractE_c2(comb_app(combS,Q2_2450),Q_2451,R_2452),
inference(superposition,[status(thm),theory(equality)],[c_13892,c_6]) ).
tff(c_324,plain,
! [Q_197,R_198] : ~ ap_contractE_c2(combS,Q_197,R_198),
inference(superposition,[status(thm),theory(equality)],[c_272,c_6]) ).
tff(c_49,plain,
! [P_56,Q_57,R_58] :
( member(pair(P_56,ap_contractE_sk2q(P_56,Q_57,R_58)),contract)
| ~ ap_contractE_c3(P_56,Q_57,R_58) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_402,plain,
! [P_222,Q_223,R_224] :
( ap_contractE_c4(P_222,Q_223,R_224)
| ap_contractE_c3(P_222,Q_223,R_224)
| ap_contractE_c2(P_222,Q_223,R_224)
| ap_contractE_c1(P_222,Q_223,R_224)
| ~ member(pair(comb_app(P_222,Q_223),R_224),contract) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_3006,plain,
! [P_878,Q_879,Q_880,R_881] :
( ap_contractE_c4(P_878,Q_879,ap_contractE_sk2q(comb_app(P_878,Q_879),Q_880,R_881))
| ap_contractE_c3(P_878,Q_879,ap_contractE_sk2q(comb_app(P_878,Q_879),Q_880,R_881))
| ap_contractE_c2(P_878,Q_879,ap_contractE_sk2q(comb_app(P_878,Q_879),Q_880,R_881))
| ap_contractE_c1(P_878,Q_879,ap_contractE_sk2q(comb_app(P_878,Q_879),Q_880,R_881))
| ~ ap_contractE_c3(comb_app(P_878,Q_879),Q_880,R_881) ),
inference(resolution,[status(thm)],[c_49,c_402]) ).
tff(c_213,plain,
! [Q_162,P_163,R_164] :
( member(pair(Q_162,ap_contractE_sk3q(P_163,Q_162,R_164)),contract)
| ~ ap_contractE_c4(P_163,Q_162,R_164) ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_61,plain,
! [R_74] : ~ member(pair(combK,R_74),contract),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_222,plain,
! [P_163,R_164] : ~ ap_contractE_c4(P_163,combK,R_164),
inference(resolution,[status(thm)],[c_213,c_61]) ).
tff(c_11253,plain,
! [P_1900,Q_1901,R_1902] :
( ap_contractE_c3(P_1900,combK,ap_contractE_sk2q(comb_app(P_1900,combK),Q_1901,R_1902))
| ap_contractE_c2(P_1900,combK,ap_contractE_sk2q(comb_app(P_1900,combK),Q_1901,R_1902))
| ap_contractE_c1(P_1900,combK,ap_contractE_sk2q(comb_app(P_1900,combK),Q_1901,R_1902))
| ~ ap_contractE_c3(comb_app(P_1900,combK),Q_1901,R_1902) ),
inference(resolution,[status(thm)],[c_3006,c_222]) ).
tff(c_227,plain,
! [P_174,Q_175,R_176] :
( member(pair(P_174,ap_contractE_sk2q(P_174,Q_175,R_176)),contract)
| ~ ap_contractE_c3(P_174,Q_175,R_176) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_63,plain,
! [R_75] : ~ member(pair(combS,R_75),contract),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_237,plain,
! [Q_175,R_176] : ~ ap_contractE_c3(combS,Q_175,R_176),
inference(resolution,[status(thm)],[c_227,c_63]) ).
tff(c_11293,plain,
! [Q_1901,R_1902] :
( ap_contractE_c2(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1901,R_1902))
| ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1901,R_1902))
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1901,R_1902) ),
inference(resolution,[status(thm)],[c_11253,c_237]) ).
tff(c_11387,plain,
! [Q_1903,R_1904] :
( ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1903,R_1904))
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1903,R_1904) ),
inference(negUnitSimplification,[status(thm)],[c_324,c_11293]) ).
tff(c_37,plain,
! [R_40,P_38,Q_39] :
( ( comb_app(combK,R_40) = P_38 )
| ~ ap_contractE_c1(P_38,Q_39,R_40) ),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_11390,plain,
! [Q_1903,R_1904] :
( ( comb_app(combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1903,R_1904)) = combS )
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1903,R_1904) ),
inference(resolution,[status(thm)],[c_11387,c_37]) ).
tff(c_11407,plain,
! [Q_1903,R_1904] : ~ ap_contractE_c3(comb_app(combS,combK),Q_1903,R_1904),
inference(negUnitSimplification,[status(thm)],[c_6,c_11390]) ).
tff(c_2,plain,
combS != combK,
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_65,plain,
member(pair(comb_app(comb_app(combS,combK),combK),r),contract),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_428,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(resolution,[status(thm)],[c_65,c_402]) ).
tff(c_434,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(negUnitSimplification,[status(thm)],[c_222,c_428]) ).
tff(c_816,plain,
ap_contractE_c1(comb_app(combS,combK),combK,r),
inference(splitLeft,[status(thm)],[c_434]) ).
tff(c_826,plain,
comb_app(combS,combK) = comb_app(combK,r),
inference(resolution,[status(thm)],[c_816,c_37]) ).
tff(c_10,plain,
! [Q2_12,Q1_10,P2_11,P1_9] :
( ( Q2_12 = Q1_10 )
| ( comb_app(P2_11,Q2_12) != comb_app(P1_9,Q1_10) ) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_910,plain,
! [Q2_12,P2_11] :
( ( combK = Q2_12 )
| ( comb_app(combK,r) != comb_app(P2_11,Q2_12) ) ),
inference(superposition,[status(thm),theory(equality)],[c_826,c_10]) ).
tff(c_966,plain,
r = combK,
inference(reflexivity,[status(thm),theory(equality)],[c_910]) ).
tff(c_898,plain,
! [P2_7,Q2_8] :
( ( combS = P2_7 )
| ( comb_app(combK,r) != comb_app(P2_7,Q2_8) ) ),
inference(superposition,[status(thm),theory(equality)],[c_826,c_8]) ).
tff(c_1145,plain,
! [P2_7,Q2_8] :
( ( combS = P2_7 )
| ( comb_app(combK,combK) != comb_app(P2_7,Q2_8) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_966,c_898]) ).
tff(c_1148,plain,
combS = combK,
inference(reflexivity,[status(thm),theory(equality)],[c_1145]) ).
tff(c_1150,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_1148]) ).
tff(c_1151,plain,
( ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c3(comb_app(combS,combK),combK,r) ),
inference(splitRight,[status(thm)],[c_434]) ).
tff(c_1153,plain,
ap_contractE_c3(comb_app(combS,combK),combK,r),
inference(splitLeft,[status(thm)],[c_1151]) ).
tff(c_11412,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11407,c_1153]) ).
tff(c_11413,plain,
ap_contractE_c2(comb_app(combS,combK),combK,r),
inference(splitRight,[status(thm)],[c_1151]) ).
tff(c_14175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14173,c_11413]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COL090-1 : TPTP v9.0.0. Released v2.7.0.
% 0.07/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 : n029.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:03:04 EDT 2025
% 0.12/0.34 % CPUTime :
% 14.51/4.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.51/4.94
% 14.51/4.94 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------