%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL090-3 : 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 : n018.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 10.08s 3.47s
% Output : CNFRefutation 10.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 11
% Syntax : Number of formulae : 47 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 87 ( 20 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 75 ( 35 ~; 40 |; 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 : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 84 ( 84 !; 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 > 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(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_101,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_106,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_61,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_121,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_135,axiom,
! [R] : ~ member(pair(combK,R),contract),
file(unknown,unknown) ).
tff(f_140,axiom,
! [R] : ~ member(pair(combS,R),contract),
file(unknown,unknown) ).
tff(f_76,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_141,axiom,
member(pair(comb_app(comb_app(combS,combK),combK),r),contract),
file(unknown,unknown) ).
tff(c_193,plain,
! [P_157,Q_158,R_159] :
( ( comb_app(comb_app(combS,ap_contractE_sk1p(P_157,Q_158,R_159)),ap_contractE_sk1q(P_157,Q_158,R_159)) = P_157 )
| ~ ap_contractE_c2(P_157,Q_158,R_159) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
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_209,plain,
! [P_157,Q1_6,P1_5,Q_158,R_159] :
( ( comb_app(combS,ap_contractE_sk1p(P_157,Q_158,R_159)) = P1_5 )
| ( comb_app(P1_5,Q1_6) != P_157 )
| ~ ap_contractE_c2(P_157,Q_158,R_159) ),
inference(superposition,[status(thm),theory(equality)],[c_193,c_8]) ).
tff(c_6706,plain,
! [P1_1492,Q1_1493,Q_1494,R_1495] :
( ( comb_app(combS,ap_contractE_sk1p(comb_app(P1_1492,Q1_1493),Q_1494,R_1495)) = P1_1492 )
| ~ ap_contractE_c2(comb_app(P1_1492,Q1_1493),Q_1494,R_1495) ),
inference(reflexivity,[status(thm),theory(equality)],[c_209]) ).
tff(c_6,plain,
! [P_3,Q_4] : ( comb_app(P_3,Q_4) != combS ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_6910,plain,
! [Q1_1493,Q_1494,R_1495] : ~ ap_contractE_c2(comb_app(combS,Q1_1493),Q_1494,R_1495),
inference(superposition,[status(thm),theory(equality)],[c_6706,c_6]) ).
tff(c_232,plain,
! [Q_158,R_159] : ~ ap_contractE_c2(combS,Q_158,R_159),
inference(superposition,[status(thm),theory(equality)],[c_193,c_6]) ).
tff(c_33,plain,
! [P_44,Q_45,R_46] :
( member(pair(P_44,ap_contractE_sk2q(P_44,Q_45,R_46)),contract)
| ~ ap_contractE_c3(P_44,Q_45,R_46) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_293,plain,
! [P_185,Q_186,R_187] :
( ap_contractE_c4(P_185,Q_186,R_187)
| ap_contractE_c3(P_185,Q_186,R_187)
| ap_contractE_c2(P_185,Q_186,R_187)
| ap_contractE_c1(P_185,Q_186,R_187)
| ~ member(pair(comb_app(P_185,Q_186),R_187),contract) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_1021,plain,
! [P_355,Q_356,Q_357,R_358] :
( ap_contractE_c4(P_355,Q_356,ap_contractE_sk2q(comb_app(P_355,Q_356),Q_357,R_358))
| ap_contractE_c3(P_355,Q_356,ap_contractE_sk2q(comb_app(P_355,Q_356),Q_357,R_358))
| ap_contractE_c2(P_355,Q_356,ap_contractE_sk2q(comb_app(P_355,Q_356),Q_357,R_358))
| ap_contractE_c1(P_355,Q_356,ap_contractE_sk2q(comb_app(P_355,Q_356),Q_357,R_358))
| ~ ap_contractE_c3(comb_app(P_355,Q_356),Q_357,R_358) ),
inference(resolution,[status(thm)],[c_33,c_293]) ).
tff(c_179,plain,
! [Q_145,P_146,R_147] :
( member(pair(Q_145,ap_contractE_sk3q(P_146,Q_145,R_147)),contract)
| ~ ap_contractE_c4(P_146,Q_145,R_147) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_45,plain,
! [R_62] : ~ member(pair(combK,R_62),contract),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_188,plain,
! [P_146,R_147] : ~ ap_contractE_c4(P_146,combK,R_147),
inference(resolution,[status(thm)],[c_179,c_45]) ).
tff(c_5337,plain,
! [P_1255,Q_1256,R_1257] :
( ap_contractE_c3(P_1255,combK,ap_contractE_sk2q(comb_app(P_1255,combK),Q_1256,R_1257))
| ap_contractE_c2(P_1255,combK,ap_contractE_sk2q(comb_app(P_1255,combK),Q_1256,R_1257))
| ap_contractE_c1(P_1255,combK,ap_contractE_sk2q(comb_app(P_1255,combK),Q_1256,R_1257))
| ~ ap_contractE_c3(comb_app(P_1255,combK),Q_1256,R_1257) ),
inference(resolution,[status(thm)],[c_1021,c_188]) ).
tff(c_159,plain,
! [P_134,Q_135,R_136] :
( member(pair(P_134,ap_contractE_sk2q(P_134,Q_135,R_136)),contract)
| ~ ap_contractE_c3(P_134,Q_135,R_136) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_47,plain,
! [R_63] : ~ member(pair(combS,R_63),contract),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_169,plain,
! [Q_135,R_136] : ~ ap_contractE_c3(combS,Q_135,R_136),
inference(resolution,[status(thm)],[c_159,c_47]) ).
tff(c_5363,plain,
! [Q_1256,R_1257] :
( ap_contractE_c2(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1256,R_1257))
| ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1256,R_1257))
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1256,R_1257) ),
inference(resolution,[status(thm)],[c_5337,c_169]) ).
tff(c_5436,plain,
! [Q_1258,R_1259] :
( ap_contractE_c1(combS,combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1258,R_1259))
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1258,R_1259) ),
inference(negUnitSimplification,[status(thm)],[c_232,c_5363]) ).
tff(c_21,plain,
! [R_28,P_26,Q_27] :
( ( comb_app(combK,R_28) = P_26 )
| ~ ap_contractE_c1(P_26,Q_27,R_28) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_5439,plain,
! [Q_1258,R_1259] :
( ( comb_app(combK,ap_contractE_sk2q(comb_app(combS,combK),Q_1258,R_1259)) = combS )
| ~ ap_contractE_c3(comb_app(combS,combK),Q_1258,R_1259) ),
inference(resolution,[status(thm)],[c_5436,c_21]) ).
tff(c_5452,plain,
! [Q_1258,R_1259] : ~ ap_contractE_c3(comb_app(combS,combK),Q_1258,R_1259),
inference(negUnitSimplification,[status(thm)],[c_6,c_5439]) ).
tff(c_2,plain,
combS != combK,
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_49,plain,
member(pair(comb_app(comb_app(combS,combK),combK),r),contract),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_316,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_49,c_293]) ).
tff(c_321,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_188,c_316]) ).
tff(c_575,plain,
ap_contractE_c1(comb_app(combS,combK),combK,r),
inference(splitLeft,[status(thm)],[c_321]) ).
tff(c_585,plain,
comb_app(combS,combK) = comb_app(combK,r),
inference(resolution,[status(thm)],[c_575,c_21]) ).
tff(c_639,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_585,c_8]) ).
tff(c_681,plain,
combS = combK,
inference(reflexivity,[status(thm),theory(equality)],[c_639]) ).
tff(c_683,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2,c_681]) ).
tff(c_684,plain,
( ap_contractE_c2(comb_app(combS,combK),combK,r)
| ap_contractE_c3(comb_app(combS,combK),combK,r) ),
inference(splitRight,[status(thm)],[c_321]) ).
tff(c_686,plain,
ap_contractE_c3(comb_app(combS,combK),combK,r),
inference(splitLeft,[status(thm)],[c_684]) ).
tff(c_5457,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5452,c_686]) ).
tff(c_5458,plain,
ap_contractE_c2(comb_app(combS,combK),combK,r),
inference(splitRight,[status(thm)],[c_684]) ).
tff(c_6913,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6910,c_5458]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : COL090-3 : TPTP v9.0.0. Released v2.7.0.
% 0.06/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.14/0.34 % Computer : n018.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 16:03:32 EDT 2025
% 0.14/0.34 % CPUTime :
% 10.08/3.47 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.08/3.47
% 10.08/3.47 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------