%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PLA003-1 : TPTP v9.0.0. Released v1.0.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 : n011.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 08:23:00 PM UTC 2025
% Result : Unsatisfiable 3.10s 1.82s
% Output : CNFRefutation 3.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of formulae : 23 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 36 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 29 ( 16 ~; 13 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 56 ( 56 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ can > monkey > ladder > bananas > #nlpp > the_ladder > the_bananas > nothing > l2 > l1 > l0 > floor > ceiling
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(l0,type,
l0: $i ).
tff(ladder,type,
ladder: ( $i * $i ) > $i ).
tff(monkey,type,
monkey: ( $i * $i * $i ) > $i ).
tff(the_bananas,type,
the_bananas: $i ).
tff(ceiling,type,
ceiling: $i ).
tff(bananas,type,
bananas: ( $i * $i ) > $i ).
tff(l2,type,
l2: $i ).
tff(nothing,type,
nothing: $i ).
tff(l1,type,
l1: $i ).
tff(floor,type,
floor: $i ).
tff(can,type,
can: ( $i * $i * $i ) > $o ).
tff(the_ladder,type,
the_ladder: $i ).
tff(f_70,axiom,
can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
file(unknown,unknown) ).
tff(f_49,axiom,
! [Location2,Ladder,Bananas,Location1] :
( can(monkey(Location2,floor,nothing),Ladder,Bananas)
| ~ can(monkey(Location1,floor,nothing),Ladder,Bananas) ),
file(unknown,unknown) ).
tff(f_69,axiom,
! [Location,Height,Bananas] :
( can(monkey(Location,Height,the_ladder),ladder(Location,Height),Bananas)
| ~ can(monkey(Location,Height,nothing),ladder(Location,Height),Bananas) ),
file(unknown,unknown) ).
tff(f_39,axiom,
! [Location2,Bananas,Location1] :
( can(monkey(Location2,floor,the_ladder),ladder(Location2,floor),Bananas)
| ~ can(monkey(Location1,floor,the_ladder),ladder(Location1,floor),Bananas) ),
file(unknown,unknown) ).
tff(f_54,axiom,
! [Location,Height,Bananas,Any_height] :
( can(monkey(Location,Height,nothing),ladder(Location,floor),Bananas)
| ~ can(monkey(Location,Height,the_ladder),ladder(Location,Any_height),Bananas) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [Location1,Bananas] :
( can(monkey(Location1,ceiling,nothing),ladder(Location1,floor),Bananas)
| ~ can(monkey(Location1,floor,nothing),ladder(Location1,floor),Bananas) ),
file(unknown,unknown) ).
tff(f_73,axiom,
! [Somewhere,Some_height,Ladder,What] : ~ can(monkey(Somewhere,Some_height,the_bananas),Ladder,What),
file(unknown,unknown) ).
tff(f_64,axiom,
! [Location,Height,Ladder] :
( can(monkey(Location,Height,the_bananas),Ladder,bananas(Location,Height))
| ~ can(monkey(Location,Height,nothing),Ladder,bananas(Location,Height)) ),
file(unknown,unknown) ).
tff(c_20,plain,
can(monkey(l0,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_27,plain,
! [Location1_39,Ladder_40,Bananas_41,Location2_42] :
( ~ can(monkey(Location1_39,floor,nothing),Ladder_40,Bananas_41)
| can(monkey(Location2_42,floor,nothing),Ladder_40,Bananas_41) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_30,plain,
! [Location2_42] : can(monkey(Location2_42,floor,nothing),ladder(l1,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[c_20,c_27]) ).
tff(c_48,plain,
! [Location_50,Height_51,Bananas_52] :
( ~ can(monkey(Location_50,Height_51,nothing),ladder(Location_50,Height_51),Bananas_52)
| can(monkey(Location_50,Height_51,the_ladder),ladder(Location_50,Height_51),Bananas_52) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_6,plain,
! [Location1_7,Bananas_6,Location2_5] :
( ~ can(monkey(Location1_7,floor,the_ladder),ladder(Location1_7,floor),Bananas_6)
| can(monkey(Location2_5,floor,the_ladder),ladder(Location2_5,floor),Bananas_6) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_68,plain,
! [Location2_59,Bananas_60,Location_61] :
( can(monkey(Location2_59,floor,the_ladder),ladder(Location2_59,floor),Bananas_60)
| ~ can(monkey(Location_61,floor,nothing),ladder(Location_61,floor),Bananas_60) ),
inference(resolution,[status(thm)],[c_48,c_6]) ).
tff(c_76,plain,
! [Location2_62] : can(monkey(Location2_62,floor,the_ladder),ladder(Location2_62,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[c_30,c_68]) ).
tff(c_12,plain,
! [Location_15,Height_16,Any_height_18,Bananas_17] :
( ~ can(monkey(Location_15,Height_16,the_ladder),ladder(Location_15,Any_height_18),Bananas_17)
| can(monkey(Location_15,Height_16,nothing),ladder(Location_15,floor),Bananas_17) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_85,plain,
! [Location2_63] : can(monkey(Location2_63,floor,nothing),ladder(Location2_63,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[c_76,c_12]) ).
tff(c_2,plain,
! [Location1_1,Bananas_2] :
( ~ can(monkey(Location1_1,floor,nothing),ladder(Location1_1,floor),Bananas_2)
| can(monkey(Location1_1,ceiling,nothing),ladder(Location1_1,floor),Bananas_2) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_133,plain,
! [Location2_69] : can(monkey(Location2_69,ceiling,nothing),ladder(Location2_69,floor),bananas(l2,ceiling)),
inference(resolution,[status(thm)],[c_85,c_2]) ).
tff(c_22,plain,
! [Somewhere_28,Some_height_29,Ladder_30,What_31] : ~ can(monkey(Somewhere_28,Some_height_29,the_bananas),Ladder_30,What_31),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_16,plain,
! [Location_22,Height_23,Ladder_24] :
( ~ can(monkey(Location_22,Height_23,nothing),Ladder_24,bananas(Location_22,Height_23))
| can(monkey(Location_22,Height_23,the_bananas),Ladder_24,bananas(Location_22,Height_23)) ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_23,plain,
! [Location_22,Height_23,Ladder_24] : ~ can(monkey(Location_22,Height_23,nothing),Ladder_24,bananas(Location_22,Height_23)),
inference(negUnitSimplification,[status(thm)],[c_22,c_16]) ).
tff(c_138,plain,
$false,
inference(resolution,[status(thm)],[c_133,c_23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : PLA003-1 : TPTP v9.0.0. Released v1.0.0.
% 0.10/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.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 16:31:33 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.10/1.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.10/1.83
% 3.10/1.83 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------