%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS292_1 : TPTP v9.3.0. Released v9.3.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 : n005.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 : Tue May 5 06:43:18 PM UTC 2026
% Result : Theorem 19.87s 8.75s
% Output : CNFRefutation 19.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 10
% Syntax : Number of formulae : 44 ( 21 unt; 0 typ; 0 def)
% Number of atoms : 77 ( 1 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 65 ( 32 ~; 26 |; 3 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 80 ( 5 atm; 13 fun; 29 num; 33 var)
% Number of types : 5 ( 3 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 25 ( 20 usr; 20 con; 0-2 aty)
% Number of variables : 104 ( 103 !; 1 ?; 104 :)
% Comments :
%------------------------------------------------------------------------------
%$ binary_relation_with_confidence > unary_relation_with_confidence > compose_unary_binary > compose_binary_unary > compose_binary_binary > #nlpp > inverse > usa > thomas > partof > northamerica > newyork > mary > livesin > john > is_person > is_country > is_continent > is_city > germany > europe > chicago > berlin
%Foreground sorts:
tff(binary_relation,type,
binary_relation: $tType ).
tff(unary_relation,type,
unary_relation: $tType ).
tff(thing,type,
thing: $tType ).
%Background operators:
%Foreground operators:
tff(compose_unary_binary,type,
compose_unary_binary: ( unary_relation * binary_relation ) > unary_relation ).
tff(is_continent,type,
is_continent: unary_relation ).
tff(inverse,type,
inverse: binary_relation > binary_relation ).
tff(compose_binary_unary,type,
compose_binary_unary: ( binary_relation * unary_relation ) > unary_relation ).
tff(livesin,type,
livesin: binary_relation ).
tff(unary_relation_with_confidence,type,
unary_relation_with_confidence: ( unary_relation * thing * $int ) > $o ).
tff(northamerica,type,
northamerica: thing ).
tff(john,type,
john: thing ).
tff(thomas,type,
thomas: thing ).
tff(is_city,type,
is_city: unary_relation ).
tff(usa,type,
usa: thing ).
tff(berlin,type,
berlin: thing ).
tff(chicago,type,
chicago: thing ).
tff(mary,type,
mary: thing ).
tff(is_person,type,
is_person: unary_relation ).
tff(is_country,type,
is_country: unary_relation ).
tff(germany,type,
germany: thing ).
tff(compose_binary_binary,type,
compose_binary_binary: ( binary_relation * binary_relation ) > binary_relation ).
tff(newyork,type,
newyork: thing ).
tff(binary_relation_with_confidence,type,
binary_relation_with_confidence: ( binary_relation * thing * thing * $int ) > $o ).
tff(europe,type,
europe: thing ).
tff(partof,type,
partof: binary_relation ).
tff(f_82,axiom,
binary_relation_with_confidence(livesin,john,newyork,1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
tff(f_63,axiom,
! [U: binary_relation,V: thing,W: thing,Xa: $int,Ya: $int] :
( ( binary_relation_with_confidence(U,V,W,Xa)
& $greatereq(Ya,Xa) )
=> binary_relation_with_confidence(U,V,W,Ya) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(f_88,axiom,
binary_relation_with_confidence(partof,newyork,usa,0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
tff(f_87,axiom,
binary_relation_with_confidence(partof,usa,northamerica,0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
tff(f_81,axiom,
! [U: thing,V: thing,W: thing,Xa: $int,Ya: $int] :
( ( binary_relation_with_confidence(partof,U,V,Xa)
& binary_relation_with_confidence(partof,V,W,Ya) )
=> binary_relation_with_confidence(partof,U,W,$sum(Xa,Ya)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
tff(f_39,axiom,
! [U: binary_relation,V: binary_relation,W: thing,X: thing,Y: thing,Za: $int,X1a: $int] :
( ( binary_relation_with_confidence(U,W,X,Za)
& binary_relation_with_confidence(V,X,Y,X1a) )
=> binary_relation_with_confidence(compose_binary_binary(U,V),W,Y,$sum(Za,X1a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
tff(f_89,axiom,
binary_relation_with_confidence(partof,chicago,usa,0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
tff(f_55,axiom,
! [U: binary_relation,V: thing,W: thing,Xa: $int] :
( binary_relation_with_confidence(U,V,W,Xa)
=> binary_relation_with_confidence(inverse(U),W,V,Xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(f_83,axiom,
binary_relation_with_confidence(livesin,mary,chicago,2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
tff(f_102,negated_conjecture,
~ ? [U: binary_relation] : binary_relation_with_confidence(U,john,mary,4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(c_75,plain,
binary_relation_with_confidence(livesin,john,newyork,1),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_11,plain,
! [X_28a: $int,U_25: binary_relation,V_26: thing,W_27: thing,Y_29a: $int] :
( binary_relation_with_confidence(U_25,V_26,W_27,Y_29a)
| ~ binary_relation_with_confidence(U_25,V_26,W_27,X_28a)
| ~ $greatereq(Y_29a,X_28a) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_195,plain,
! [X_72a: $int,U_70: binary_relation,Y_69a: $int,V_68: thing,W_71: thing] :
( binary_relation_with_confidence(U_70,V_68,W_71,Y_69a)
| ~ binary_relation_with_confidence(U_70,V_68,W_71,X_72a)
| $less(Y_69a,X_72a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_11]) ).
tff(c_219,plain,
! [Y_69a: $int] :
( binary_relation_with_confidence(livesin,john,newyork,Y_69a)
| $less(Y_69a,1) ),
inference(resolution,[status(thm)],[c_75,c_195]) ).
tff(c_69,plain,
binary_relation_with_confidence(partof,newyork,usa,0),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_70,plain,
binary_relation_with_confidence(partof,usa,northamerica,0),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_465,plain,
! [X_116a: $int,W_114: thing,Y_117a: $int,U_119: thing,V_118: thing] :
( binary_relation_with_confidence(partof,U_119,W_114,$sum(X_116a,Y_117a))
| ~ binary_relation_with_confidence(partof,V_118,W_114,Y_117a)
| ~ binary_relation_with_confidence(partof,U_119,V_118,X_116a) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_494,plain,
! [U_119: thing,X_116a: $int] :
( binary_relation_with_confidence(partof,U_119,northamerica,$sum(X_116a,0))
| ~ binary_relation_with_confidence(partof,U_119,usa,X_116a) ),
inference(resolution,[status(thm)],[c_70,c_465]) ).
tff(c_820,plain,
! [U_186: thing,X_187a: $int] :
( binary_relation_with_confidence(partof,U_186,northamerica,X_187a)
| ~ binary_relation_with_confidence(partof,U_186,usa,X_187a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_494]) ).
tff(c_850,plain,
binary_relation_with_confidence(partof,newyork,northamerica,0),
inference(resolution,[status(thm)],[c_69,c_820]) ).
tff(c_98,plain,
! [X1_7a: $int,W_3: thing,Y_5: thing,V_2: binary_relation,X_4: thing,Z_6a: $int,U_1: binary_relation] :
( binary_relation_with_confidence(compose_binary_binary(U_1,V_2),W_3,Y_5,$sum(Z_6a,X1_7a))
| ~ binary_relation_with_confidence(V_2,X_4,Y_5,X1_7a)
| ~ binary_relation_with_confidence(U_1,W_3,X_4,Z_6a) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_885,plain,
! [U_1: binary_relation,W_3: thing,Z_6a: $int] :
( binary_relation_with_confidence(compose_binary_binary(U_1,partof),W_3,northamerica,$sum(Z_6a,0))
| ~ binary_relation_with_confidence(U_1,W_3,newyork,Z_6a) ),
inference(resolution,[status(thm)],[c_850,c_98]) ).
tff(c_887,plain,
! [U_1: binary_relation,W_3: thing,Z_6a: $int] :
( binary_relation_with_confidence(compose_binary_binary(U_1,partof),W_3,northamerica,Z_6a)
| ~ binary_relation_with_confidence(U_1,W_3,newyork,Z_6a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_885]) ).
tff(c_68,plain,
binary_relation_with_confidence(partof,chicago,usa,0),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_848,plain,
binary_relation_with_confidence(partof,chicago,northamerica,0),
inference(resolution,[status(thm)],[c_68,c_820]) ).
tff(c_86,plain,
! [U_20: binary_relation,W_22: thing,V_21: thing,X_23a: $int] :
( binary_relation_with_confidence(inverse(U_20),W_22,V_21,X_23a)
| ~ binary_relation_with_confidence(U_20,V_21,W_22,X_23a) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_665,plain,
! [Z_162a: $int,V_159: binary_relation,Y_156: thing,U_157: binary_relation,X_155: thing,X1_161a: $int,W_158: thing] :
( binary_relation_with_confidence(compose_binary_binary(U_157,V_159),W_158,Y_156,$sum(Z_162a,X1_161a))
| ~ binary_relation_with_confidence(V_159,X_155,Y_156,X1_161a)
| ~ binary_relation_with_confidence(U_157,W_158,X_155,Z_162a) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_732,plain,
! [Z_162a: $int,U_157: binary_relation,U_20: binary_relation,W_22: thing,V_21: thing,W_158: thing,X_23a: $int] :
( binary_relation_with_confidence(compose_binary_binary(U_157,inverse(U_20)),W_158,V_21,$sum(Z_162a,X_23a))
| ~ binary_relation_with_confidence(U_157,W_158,W_22,Z_162a)
| ~ binary_relation_with_confidence(U_20,V_21,W_22,X_23a) ),
inference(resolution,[status(thm)],[c_86,c_665]) ).
tff(c_5421,plain,
! [X_760a: $int,V_767: thing,W_762: thing,U_763: binary_relation,W_765: thing,U_764: binary_relation,Z_761a: $int] :
( binary_relation_with_confidence(compose_binary_binary(U_763,inverse(U_764)),W_765,V_767,$sum(X_760a,Z_761a))
| ~ binary_relation_with_confidence(U_763,W_765,W_762,Z_761a)
| ~ binary_relation_with_confidence(U_764,V_767,W_762,X_760a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_732]) ).
tff(c_5670,plain,
! [U_764: binary_relation,V_767: thing,X_760a: $int] :
( binary_relation_with_confidence(compose_binary_binary(partof,inverse(U_764)),chicago,V_767,$sum(X_760a,0))
| ~ binary_relation_with_confidence(U_764,V_767,northamerica,X_760a) ),
inference(resolution,[status(thm)],[c_848,c_5421]) ).
tff(c_5672,plain,
! [U_764: binary_relation,V_767: thing,X_760a: $int] :
( binary_relation_with_confidence(compose_binary_binary(partof,inverse(U_764)),chicago,V_767,X_760a)
| ~ binary_relation_with_confidence(U_764,V_767,northamerica,X_760a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5670]) ).
tff(c_74,plain,
binary_relation_with_confidence(livesin,mary,chicago,2),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_5730,plain,
! [U_764: binary_relation,V_767: thing,X_760a: $int] :
( binary_relation_with_confidence(compose_binary_binary(livesin,inverse(U_764)),mary,V_767,$sum(X_760a,2))
| ~ binary_relation_with_confidence(U_764,V_767,chicago,X_760a) ),
inference(resolution,[status(thm)],[c_74,c_5421]) ).
tff(c_27394,plain,
! [U_3424: binary_relation,V_3425: thing,X_3427a: $int] :
( binary_relation_with_confidence(compose_binary_binary(livesin,inverse(U_3424)),mary,V_3425,$sum(2,X_3427a))
| ~ binary_relation_with_confidence(U_3424,V_3425,chicago,X_3427a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5730]) ).
tff(c_127,plain,
! [U_57: binary_relation,W_58: thing,V_59: thing,X_60a: $int] :
( binary_relation_with_confidence(inverse(U_57),W_58,V_59,X_60a)
| ~ binary_relation_with_confidence(U_57,V_59,W_58,X_60a) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_57,plain,
! [U_44: binary_relation] : ~ binary_relation_with_confidence(U_44,john,mary,4),
inference(cnfTransformation,[status(thm)],[f_102]) ).
tff(c_136,plain,
! [U_57: binary_relation] : ~ binary_relation_with_confidence(U_57,mary,john,4),
inference(resolution,[status(thm)],[c_127,c_57]) ).
tff(c_27902,plain,
! [X_3427a: $int,U_3424: binary_relation] :
( ( $sum(2,X_3427a) != 4 )
| ~ binary_relation_with_confidence(U_3424,john,chicago,X_3427a) ),
inference(resolution,[status(thm)],[c_27394,c_136]) ).
tff(c_27909,plain,
! [U_3472: binary_relation] : ~ binary_relation_with_confidence(U_3472,john,chicago,2),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_27902]) ).
tff(c_27962,plain,
! [U_3474: binary_relation] : ~ binary_relation_with_confidence(U_3474,chicago,john,2),
inference(resolution,[status(thm)],[c_86,c_27909]) ).
tff(c_28036,plain,
! [U_3477: binary_relation] : ~ binary_relation_with_confidence(U_3477,john,northamerica,2),
inference(resolution,[status(thm)],[c_5672,c_27962]) ).
tff(c_28269,plain,
! [U_3480: binary_relation] : ~ binary_relation_with_confidence(U_3480,john,newyork,2),
inference(resolution,[status(thm)],[c_887,c_28036]) ).
tff(c_28304,plain,
$less(2,1),
inference(resolution,[status(thm)],[c_219,c_28269]) ).
tff(c_28307,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_28304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS292_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/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.16/0.34 % Computer : n005.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 03:37:15 EDT 2026
% 0.16/0.35 % CPUTime :
% 19.87/8.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.87/8.76
% 19.87/8.76 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------