%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COL092-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 6.52s 2.42s
% Output : CNFRefutation 6.52s
% 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_28,axiom,
! [P,Q] : ( combK != 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(combK,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(combK,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_233,axiom,
! [R] :
( ~ member(pair(combK,R),parcontract)
| ( R = combK ) ),
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_4,plain,
! [P_1,Q_2] : ( comb_app(P_1,Q_2) != combK ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
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(combK,PP_191) != r ) ),
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_167,plain,
( ( comb_app(combK,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_527,plain,
! [Q_319,R_320] : ~ ap_parcontractE_c3(combK,Q_319,R_320),
inference(superposition,[status(thm),theory(equality)],[c_472,c_4]) ).
tff(c_109,plain,
member(pair(comb_app(combK,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(combK,p,r)
| ap_parcontractE_c3(combK,p,r)
| ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c1(combK,p,r) ),
inference(resolution,[status(thm)],[c_109,c_915]) ).
tff(c_965,plain,
( ap_parcontractE_c4(combK,p,r)
| ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c1(combK,p,r) ),
inference(negUnitSimplification,[status(thm)],[c_527,c_957]) ).
tff(c_966,plain,
ap_parcontractE_c1(combK,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(combK,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_1036,plain,
( member(p,comb)
| ~ member(r,comb) ),
inference(superposition,[status(thm),theory(equality)],[c_973,c_17]) ).
tff(c_1056,plain,
~ member(r,comb),
inference(negUnitSimplification,[status(thm)],[c_169,c_1036]) ).
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(combK,p),comb),
inference(resolution,[status(thm)],[c_966,c_83]) ).
tff(c_1139,plain,
member(r,comb),
inference(demodulation,[status(thm),theory(equality)],[c_973,c_972]) ).
tff(c_1140,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1056,c_1139]) ).
tff(c_1141,plain,
( ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c4(combK,p,r) ),
inference(splitRight,[status(thm)],[c_965]) ).
tff(c_1214,plain,
ap_parcontractE_c4(combK,p,r),
inference(splitLeft,[status(thm)],[c_1141]) ).
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_75,plain,
! [R_87] :
( ( combK = R_87 )
| ~ member(pair(combK,R_87),parcontract) ),
inference(cnfTransformation,[status(thm)],[f_233]) ).
tff(c_340,plain,
! [Q_262,R_263] :
( ( ap_parcontractE_sk2q(combK,Q_262,R_263) = combK )
| ~ ap_parcontractE_c4(combK,Q_262,R_263) ),
inference(resolution,[status(thm)],[c_326,c_75]) ).
tff(c_1229,plain,
ap_parcontractE_sk2q(combK,p,r) = combK,
inference(resolution,[status(thm)],[c_1214,c_340]) ).
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_1236,plain,
( ( comb_app(combK,ap_parcontractE_sk2s(combK,p,r)) = r )
| ~ ap_parcontractE_c4(combK,p,r) ),
inference(superposition,[status(thm),theory(equality)],[c_1229,c_107]) ).
tff(c_1245,plain,
comb_app(combK,ap_parcontractE_sk2s(combK,p,r)) = r,
inference(demodulation,[status(thm),theory(equality)],[c_1214,c_1236]) ).
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(combK,PP_132) != r ) ),
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_300,plain,
! [P_239,R_240] :
( ( comb_app(combK,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_1376,plain,
~ ap_parcontractE_c4(combK,p,r),
inference(superposition,[status(thm),theory(equality)],[c_1245,c_300]) ).
tff(c_1429,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1214,c_1376]) ).
tff(c_1430,plain,
ap_parcontractE_c2(combK,p,r),
inference(splitRight,[status(thm)],[c_1141]) ).
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_1505,plain,
comb_app(combK,r) = combK,
inference(resolution,[status(thm)],[c_1430,c_91]) ).
tff(c_1515,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_1505]) ).
tff(c_1516,plain,
comb_app(combK,p) != r,
inference(splitRight,[status(thm)],[c_167]) ).
tff(c_1820,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_1875,plain,
! [Q_549,R_550] : ~ ap_parcontractE_c3(combK,Q_549,R_550),
inference(superposition,[status(thm),theory(equality)],[c_1820,c_4]) ).
tff(c_2263,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_2305,plain,
( ap_parcontractE_c4(combK,p,r)
| ap_parcontractE_c3(combK,p,r)
| ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c1(combK,p,r) ),
inference(resolution,[status(thm)],[c_109,c_2263]) ).
tff(c_2313,plain,
( ap_parcontractE_c4(combK,p,r)
| ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c1(combK,p,r) ),
inference(negUnitSimplification,[status(thm)],[c_1875,c_2305]) ).
tff(c_2314,plain,
ap_parcontractE_c1(combK,p,r),
inference(splitLeft,[status(thm)],[c_2313]) ).
tff(c_2319,plain,
comb_app(combK,p) = r,
inference(resolution,[status(thm)],[c_2314,c_85]) ).
tff(c_2324,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1516,c_2319]) ).
tff(c_2325,plain,
( ap_parcontractE_c2(combK,p,r)
| ap_parcontractE_c4(combK,p,r) ),
inference(splitRight,[status(thm)],[c_2313]) ).
tff(c_2327,plain,
ap_parcontractE_c4(combK,p,r),
inference(splitLeft,[status(thm)],[c_2325]) ).
tff(c_1675,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_1689,plain,
! [Q_497,R_498] :
( ( ap_parcontractE_sk2q(combK,Q_497,R_498) = combK )
| ~ ap_parcontractE_c4(combK,Q_497,R_498) ),
inference(resolution,[status(thm)],[c_1675,c_75]) ).
tff(c_2342,plain,
ap_parcontractE_sk2q(combK,p,r) = combK,
inference(resolution,[status(thm)],[c_2327,c_1689]) ).
tff(c_2420,plain,
( ( comb_app(combK,ap_parcontractE_sk2s(combK,p,r)) = r )
| ~ ap_parcontractE_c4(combK,p,r) ),
inference(superposition,[status(thm),theory(equality)],[c_2342,c_107]) ).
tff(c_2429,plain,
comb_app(combK,ap_parcontractE_sk2s(combK,p,r)) = r,
inference(demodulation,[status(thm),theory(equality)],[c_2327,c_2420]) ).
tff(c_1657,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_1670,plain,
! [P_490,R_491] :
( ( comb_app(combK,ap_parcontractE_sk2s(P_490,p,R_491)) != r )
| ~ ap_parcontractE_c4(P_490,p,R_491) ),
inference(resolution,[status(thm)],[c_1657,c_111]) ).
tff(c_2560,plain,
~ ap_parcontractE_c4(combK,p,r),
inference(superposition,[status(thm),theory(equality)],[c_2429,c_1670]) ).
tff(c_2613,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2327,c_2560]) ).
tff(c_2614,plain,
ap_parcontractE_c2(combK,p,r),
inference(splitRight,[status(thm)],[c_2325]) ).
tff(c_2618,plain,
comb_app(combK,r) = combK,
inference(resolution,[status(thm)],[c_2614,c_91]) ).
tff(c_2628,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4,c_2618]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : COL092-1 : TPTP v9.0.0. Released v2.7.0.
% 0.00/0.09 % 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.08/0.28 % Computer : n029.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Mon Apr 7 16:03:19 EDT 2025
% 0.08/0.28 % CPUTime :
% 6.52/2.42 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.52/2.43
% 6.52/2.43 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------