%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL093-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/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:02 PM UTC 2025
% Result : Unsatisfiable 7.36s 2.91s
% Output : CNFRefutation 7.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of formulae : 76 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 134 ( 32 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 110 ( 52 ~; 58 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 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 : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-3 aty)
% Number of variables : 87 ( 87 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ ap_parcontractE_c4 > ap_parcontractE_c3 > ap_parcontractE_c2 > ap_parcontractE_c1 > ap_contractE_c4 > ap_contractE_c3 > ap_contractE_c2 > ap_contractE_c1 > member > ap_parcontractE_sk2s > ap_parcontractE_sk2q > ap_parcontractE_sk1q > ap_parcontractE_sk1p > ap_contractE_sk3q > ap_contractE_sk2q > ap_contractE_sk1q > ap_contractE_sk1p > pair > comb_app > #nlpp > rtrancl > r > parcontract > p > contract > combS > combK > comb
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(ap_parcontractE_sk1p,type,
ap_parcontractE_sk1p: ( $i * $i * $i ) > $i ).
tff(ap_parcontractE_sk2q,type,
ap_parcontractE_sk2q: ( $i * $i * $i ) > $i ).
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(parcontract,type,
parcontract: $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(ap_parcontractE_c3,type,
ap_parcontractE_c3: ( $i * $i * $i ) > $o ).
tff(ap_parcontractE_c2,type,
ap_parcontractE_c2: ( $i * $i * $i ) > $o ).
tff(pair,type,
pair: ( $i * $i ) > $i ).
tff(ap_parcontractE_c1,type,
ap_parcontractE_c1: ( $i * $i * $i ) > $o ).
tff(contract,type,
contract: $i ).
tff(ap_contractE_c2,type,
ap_contractE_c2: ( $i * $i * $i ) > $o ).
tff(ap_parcontractE_c4,type,
ap_parcontractE_c4: ( $i * $i * $i ) > $o ).
tff(combK,type,
combK: $i ).
tff(ap_parcontractE_sk1q,type,
ap_parcontractE_sk1q: ( $i * $i * $i ) > $i ).
tff(p,type,
p: $i ).
tff(ap_parcontractE_sk2s,type,
ap_parcontractE_sk2s: ( $i * $i * $i ) > $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_31,axiom,
! [P,Q] : ( combS != comb_app(P,Q) ),
file(unknown,unknown) ).
tff(f_195,axiom,
! [P] :
( ~ member(P,comb)
| member(pair(P,P),parcontract) ),
file(unknown,unknown) ).
tff(f_328,axiom,
! [PP] :
( ( r != comb_app(combS,PP) )
| ~ member(pair(p,PP),parcontract) ),
file(unknown,unknown) ).
tff(f_306,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c3(P,Q,R)
| ( P = comb_app(comb_app(combS,ap_parcontractE_sk1p(P,Q,R)),ap_parcontractE_sk1q(P,Q,R)) ) ),
file(unknown,unknown) ).
tff(f_322,axiom,
member(pair(comb_app(combS,p),r),parcontract),
file(unknown,unknown) ).
tff(f_256,axiom,
! [P,Q,R] :
( ~ member(pair(comb_app(P,Q),R),parcontract)
| ap_parcontractE_c1(P,Q,R)
| ap_parcontractE_c2(P,Q,R)
| ap_parcontractE_c3(P,Q,R)
| ap_parcontractE_c4(P,Q,R) ),
file(unknown,unknown) ).
tff(f_266,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c1(P,Q,R)
| ( R = comb_app(P,Q) ) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [P,Q] :
( ~ member(comb_app(P,Q),comb)
| member(Q,comb) ),
file(unknown,unknown) ).
tff(f_261,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c1(P,Q,R)
| member(comb_app(P,Q),comb) ),
file(unknown,unknown) ).
tff(f_311,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c4(P,Q,R)
| member(pair(P,ap_parcontractE_sk2q(P,Q,R)),parcontract) ),
file(unknown,unknown) ).
tff(f_244,axiom,
! [R] :
( ~ member(pair(combS,R),parcontract)
| ( R = combS ) ),
file(unknown,unknown) ).
tff(f_321,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c4(P,Q,R)
| ( R = comb_app(ap_parcontractE_sk2q(P,Q,R),ap_parcontractE_sk2s(P,Q,R)) ) ),
file(unknown,unknown) ).
tff(f_316,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c4(P,Q,R)
| member(pair(Q,ap_parcontractE_sk2s(P,Q,R)),parcontract) ),
file(unknown,unknown) ).
tff(f_281,axiom,
! [P,Q,R] :
( ~ ap_parcontractE_c2(P,Q,R)
| ( P = comb_app(combK,R) ) ),
file(unknown,unknown) ).
tff(c_6,plain,
! [P_3,Q_4] : ( comb_app(P_3,Q_4) != combS ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_65,plain,
! [P_76] :
( member(pair(P_76,P_76),parcontract)
| ~ member(P_76,comb) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_162,plain,
! [PP_191] :
( ~ member(pair(p,PP_191),parcontract)
| ( comb_app(combS,PP_191) != r ) ),
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_167,plain,
( ( comb_app(combS,p) != r )
| ~ member(p,comb) ),
inference(resolution,[status(thm)],[c_65,c_162]) ).
tff(c_169,plain,
~ member(p,comb),
inference(splitLeft,[status(thm)],[c_167]) ).
tff(c_472,plain,
! [P_318,Q_319,R_320] :
( ( comb_app(comb_app(combS,ap_parcontractE_sk1p(P_318,Q_319,R_320)),ap_parcontractE_sk1q(P_318,Q_319,R_320)) = P_318 )
| ~ ap_parcontractE_c3(P_318,Q_319,R_320) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_529,plain,
! [Q_319,R_320] : ~ ap_parcontractE_c3(combS,Q_319,R_320),
inference(superposition,[status(thm),theory(equality)],[c_472,c_6]) ).
tff(c_109,plain,
member(pair(comb_app(combS,p),r),parcontract),
inference(cnfTransformation,[status(thm)],[f_322]) ).
tff(c_915,plain,
! [P_410,Q_411,R_412] :
( ap_parcontractE_c4(P_410,Q_411,R_412)
| ap_parcontractE_c3(P_410,Q_411,R_412)
| ap_parcontractE_c2(P_410,Q_411,R_412)
| ap_parcontractE_c1(P_410,Q_411,R_412)
| ~ member(pair(comb_app(P_410,Q_411),R_412),parcontract) ),
inference(cnfTransformation,[status(thm)],[f_256]) ).
tff(c_957,plain,
( ap_parcontractE_c4(combS,p,r)
| ap_parcontractE_c3(combS,p,r)
| ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c1(combS,p,r) ),
inference(resolution,[status(thm)],[c_109,c_915]) ).
tff(c_965,plain,
( ap_parcontractE_c4(combS,p,r)
| ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c1(combS,p,r) ),
inference(negUnitSimplification,[status(thm)],[c_529,c_957]) ).
tff(c_966,plain,
ap_parcontractE_c1(combS,p,r),
inference(splitLeft,[status(thm)],[c_965]) ).
tff(c_85,plain,
! [P_96,Q_97,R_98] :
( ( comb_app(P_96,Q_97) = R_98 )
| ~ ap_parcontractE_c1(P_96,Q_97,R_98) ),
inference(cnfTransformation,[status(thm)],[f_266]) ).
tff(c_973,plain,
comb_app(combS,p) = r,
inference(resolution,[status(thm)],[c_966,c_85]) ).
tff(c_17,plain,
! [Q_20,P_19] :
( member(Q_20,comb)
| ~ member(comb_app(P_19,Q_20),comb) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_1030,plain,
( member(p,comb)
| ~ member(r,comb) ),
inference(superposition,[status(thm),theory(equality)],[c_973,c_17]) ).
tff(c_1050,plain,
~ member(r,comb),
inference(negUnitSimplification,[status(thm)],[c_169,c_1030]) ).
tff(c_83,plain,
! [P_93,Q_94,R_95] :
( member(comb_app(P_93,Q_94),comb)
| ~ ap_parcontractE_c1(P_93,Q_94,R_95) ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_972,plain,
member(comb_app(combS,p),comb),
inference(resolution,[status(thm)],[c_966,c_83]) ).
tff(c_1136,plain,
member(r,comb),
inference(demodulation,[status(thm),theory(equality)],[c_973,c_972]) ).
tff(c_1137,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1050,c_1136]) ).
tff(c_1138,plain,
( ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c4(combS,p,r) ),
inference(splitRight,[status(thm)],[c_965]) ).
tff(c_1211,plain,
ap_parcontractE_c4(combS,p,r),
inference(splitLeft,[status(thm)],[c_1138]) ).
tff(c_326,plain,
! [P_261,Q_262,R_263] :
( member(pair(P_261,ap_parcontractE_sk2q(P_261,Q_262,R_263)),parcontract)
| ~ ap_parcontractE_c4(P_261,Q_262,R_263) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_79,plain,
! [R_89] :
( ( combS = R_89 )
| ~ member(pair(combS,R_89),parcontract) ),
inference(cnfTransformation,[status(thm)],[f_244]) ).
tff(c_341,plain,
! [Q_262,R_263] :
( ( ap_parcontractE_sk2q(combS,Q_262,R_263) = combS )
| ~ ap_parcontractE_c4(combS,Q_262,R_263) ),
inference(resolution,[status(thm)],[c_326,c_79]) ).
tff(c_1226,plain,
ap_parcontractE_sk2q(combS,p,r) = combS,
inference(resolution,[status(thm)],[c_1211,c_341]) ).
tff(c_107,plain,
! [P_129,Q_130,R_131] :
( ( comb_app(ap_parcontractE_sk2q(P_129,Q_130,R_131),ap_parcontractE_sk2s(P_129,Q_130,R_131)) = R_131 )
| ~ ap_parcontractE_c4(P_129,Q_130,R_131) ),
inference(cnfTransformation,[status(thm)],[f_321]) ).
tff(c_1233,plain,
( ( comb_app(combS,ap_parcontractE_sk2s(combS,p,r)) = r )
| ~ ap_parcontractE_c4(combS,p,r) ),
inference(superposition,[status(thm),theory(equality)],[c_1226,c_107]) ).
tff(c_1242,plain,
comb_app(combS,ap_parcontractE_sk2s(combS,p,r)) = r,
inference(demodulation,[status(thm),theory(equality)],[c_1211,c_1233]) ).
tff(c_287,plain,
! [Q_238,P_239,R_240] :
( member(pair(Q_238,ap_parcontractE_sk2s(P_239,Q_238,R_240)),parcontract)
| ~ ap_parcontractE_c4(P_239,Q_238,R_240) ),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_111,plain,
! [PP_132] :
( ~ member(pair(p,PP_132),parcontract)
| ( comb_app(combS,PP_132) != r ) ),
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_300,plain,
! [P_239,R_240] :
( ( comb_app(combS,ap_parcontractE_sk2s(P_239,p,R_240)) != r )
| ~ ap_parcontractE_c4(P_239,p,R_240) ),
inference(resolution,[status(thm)],[c_287,c_111]) ).
tff(c_1373,plain,
~ ap_parcontractE_c4(combS,p,r),
inference(superposition,[status(thm),theory(equality)],[c_1242,c_300]) ).
tff(c_1426,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1211,c_1373]) ).
tff(c_1427,plain,
ap_parcontractE_c2(combS,p,r),
inference(splitRight,[status(thm)],[c_1138]) ).
tff(c_91,plain,
! [R_107,P_105,Q_106] :
( ( comb_app(combK,R_107) = P_105 )
| ~ ap_parcontractE_c2(P_105,Q_106,R_107) ),
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_1502,plain,
comb_app(combK,r) = combS,
inference(resolution,[status(thm)],[c_1427,c_91]) ).
tff(c_1512,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_1502]) ).
tff(c_1513,plain,
comb_app(combS,p) != r,
inference(splitRight,[status(thm)],[c_167]) ).
tff(c_1817,plain,
! [P_548,Q_549,R_550] :
( ( comb_app(comb_app(combS,ap_parcontractE_sk1p(P_548,Q_549,R_550)),ap_parcontractE_sk1q(P_548,Q_549,R_550)) = P_548 )
| ~ ap_parcontractE_c3(P_548,Q_549,R_550) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_1874,plain,
! [Q_549,R_550] : ~ ap_parcontractE_c3(combS,Q_549,R_550),
inference(superposition,[status(thm),theory(equality)],[c_1817,c_6]) ).
tff(c_2260,plain,
! [P_640,Q_641,R_642] :
( ap_parcontractE_c4(P_640,Q_641,R_642)
| ap_parcontractE_c3(P_640,Q_641,R_642)
| ap_parcontractE_c2(P_640,Q_641,R_642)
| ap_parcontractE_c1(P_640,Q_641,R_642)
| ~ member(pair(comb_app(P_640,Q_641),R_642),parcontract) ),
inference(cnfTransformation,[status(thm)],[f_256]) ).
tff(c_2302,plain,
( ap_parcontractE_c4(combS,p,r)
| ap_parcontractE_c3(combS,p,r)
| ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c1(combS,p,r) ),
inference(resolution,[status(thm)],[c_109,c_2260]) ).
tff(c_2310,plain,
( ap_parcontractE_c4(combS,p,r)
| ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c1(combS,p,r) ),
inference(negUnitSimplification,[status(thm)],[c_1874,c_2302]) ).
tff(c_2311,plain,
ap_parcontractE_c1(combS,p,r),
inference(splitLeft,[status(thm)],[c_2310]) ).
tff(c_2316,plain,
comb_app(combS,p) = r,
inference(resolution,[status(thm)],[c_2311,c_85]) ).
tff(c_2321,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1513,c_2316]) ).
tff(c_2322,plain,
( ap_parcontractE_c2(combS,p,r)
| ap_parcontractE_c4(combS,p,r) ),
inference(splitRight,[status(thm)],[c_2310]) ).
tff(c_2324,plain,
ap_parcontractE_c4(combS,p,r),
inference(splitLeft,[status(thm)],[c_2322]) ).
tff(c_1672,plain,
! [P_496,Q_497,R_498] :
( member(pair(P_496,ap_parcontractE_sk2q(P_496,Q_497,R_498)),parcontract)
| ~ ap_parcontractE_c4(P_496,Q_497,R_498) ),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_1687,plain,
! [Q_497,R_498] :
( ( ap_parcontractE_sk2q(combS,Q_497,R_498) = combS )
| ~ ap_parcontractE_c4(combS,Q_497,R_498) ),
inference(resolution,[status(thm)],[c_1672,c_79]) ).
tff(c_2339,plain,
ap_parcontractE_sk2q(combS,p,r) = combS,
inference(resolution,[status(thm)],[c_2324,c_1687]) ).
tff(c_2417,plain,
( ( comb_app(combS,ap_parcontractE_sk2s(combS,p,r)) = r )
| ~ ap_parcontractE_c4(combS,p,r) ),
inference(superposition,[status(thm),theory(equality)],[c_2339,c_107]) ).
tff(c_2426,plain,
comb_app(combS,ap_parcontractE_sk2s(combS,p,r)) = r,
inference(demodulation,[status(thm),theory(equality)],[c_2324,c_2417]) ).
tff(c_1654,plain,
! [Q_489,P_490,R_491] :
( member(pair(Q_489,ap_parcontractE_sk2s(P_490,Q_489,R_491)),parcontract)
| ~ ap_parcontractE_c4(P_490,Q_489,R_491) ),
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_1667,plain,
! [P_490,R_491] :
( ( comb_app(combS,ap_parcontractE_sk2s(P_490,p,R_491)) != r )
| ~ ap_parcontractE_c4(P_490,p,R_491) ),
inference(resolution,[status(thm)],[c_1654,c_111]) ).
tff(c_2557,plain,
~ ap_parcontractE_c4(combS,p,r),
inference(superposition,[status(thm),theory(equality)],[c_2426,c_1667]) ).
tff(c_2610,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2324,c_2557]) ).
tff(c_2611,plain,
ap_parcontractE_c2(combS,p,r),
inference(splitRight,[status(thm)],[c_2322]) ).
tff(c_2615,plain,
comb_app(combK,r) = combS,
inference(resolution,[status(thm)],[c_2611,c_91]) ).
tff(c_2625,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6,c_2615]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COL093-1 : TPTP v9.0.0. Released v2.7.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/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:04:01 EDT 2025
% 0.12/0.34 % CPUTime :
% 7.36/2.91 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.36/2.91
% 7.36/2.91 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------