%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX186-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 : 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 : Tue May 5 06:56:33 PM UTC 2026
% Result : Unsatisfiable 2.93s 1.78s
% Output : CNFRefutation 3.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of formulae : 22 ( 22 unt; 0 typ; 0 def)
% Number of atoms : 22 ( 21 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 40 ( 40 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ prop_drop_inj2 > impl > eq3 > eq2 > eq > drop > cons > #nlpp > s > z > nil > btrue > bfalse
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(eq,type,
eq: ( $i * $i ) > $i ).
tff(eq3,type,
eq3: ( $i * $i ) > $i ).
tff(s,type,
s: $i > $i ).
tff(prop_drop_inj2,type,
prop_drop_inj2: ( $i * $i * $i ) > $i ).
tff(drop,type,
drop: ( $i * $i ) > $i ).
tff(impl,type,
impl: ( $i * $i ) > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(z,type,
z: $i ).
tff(bfalse,type,
bfalse: $i ).
tff(eq2,type,
eq2: ( $i * $i ) > $i ).
tff(nil,type,
nil: $i ).
tff(btrue,type,
btrue: $i ).
tff(f_47,axiom,
! [X] : ( eq3(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [Q] : ( impl(btrue,Q) = Q ),
file(unknown,unknown) ).
tff(f_43,axiom,
! [X] : ( eq(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [Z] : ( drop(s(Z),nil) = nil ),
file(unknown,unknown) ).
tff(f_59,axiom,
! [X,Y] : ( eq(nil,cons(X,Y)) = bfalse ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [Z,X2,X3] : ( drop(s(Z),cons(X2,X3)) = drop(Z,X3) ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [X,Y,Z] : ( prop_drop_inj2(X,Y,Z) = impl(eq(drop(X,Y),drop(X,Z)),eq(Y,Z)) ),
file(unknown,unknown) ).
tff(f_64,axiom,
! [X,Y,Z] : ( eq3(prop_drop_inj2(X,Y,Z),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_28,plain,
! [X_17] : ( eq3(X_17,X_17) = btrue ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_2,plain,
! [Q_1] : ( impl(btrue,Q_1) = Q_1 ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_24,plain,
! [X_15] : ( eq(X_15,X_15) = btrue ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_6,plain,
! [Z_3] : ( drop(s(Z_3),nil) = nil ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_34,plain,
! [X_26,Y_27] : ( eq(nil,cons(X_26,Y_27)) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_8,plain,
! [Z_4,X2_5,X3_6] : ( drop(s(Z_4),cons(X2_5,X3_6)) = drop(Z_4,X3_6) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_204,plain,
! [X_62,Y_63,Z_64] : ( impl(eq(drop(X_62,Y_63),drop(X_62,Z_64)),eq(Y_63,Z_64)) = prop_drop_inj2(X_62,Y_63,Z_64) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_376,plain,
! [Z_79,Z_80] : ( impl(eq(nil,drop(s(Z_79),Z_80)),eq(nil,Z_80)) = prop_drop_inj2(s(Z_79),nil,Z_80) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_204]) ).
tff(c_385,plain,
! [Z_4,X3_6,X2_5] : ( impl(eq(nil,drop(Z_4,X3_6)),eq(nil,cons(X2_5,X3_6))) = prop_drop_inj2(s(Z_4),nil,cons(X2_5,X3_6)) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_376]) ).
tff(c_402,plain,
! [Z_81,X2_82,X3_83] : ( prop_drop_inj2(s(Z_81),nil,cons(X2_82,X3_83)) = impl(eq(nil,drop(Z_81,X3_83)),bfalse) ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_385]) ).
tff(c_38,plain,
! [X_30,Y_31,Z_32] : ( eq3(prop_drop_inj2(X_30,Y_31,Z_32),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_413,plain,
! [Z_84,X3_85] : ( eq3(impl(eq(nil,drop(Z_84,X3_85)),bfalse),bfalse) != btrue ),
inference(superposition,[status(thm),theory(equality)],[c_402,c_38]) ).
tff(c_417,plain,
eq3(impl(eq(nil,nil),bfalse),bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_6,c_413]) ).
tff(c_422,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_2,c_24,c_417]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX186-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/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.15/0.34 % Computer : n029.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 09:38:59 EDT 2026
% 0.15/0.34 % CPUTime :
% 2.93/1.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.93/1.79
% 2.93/1.79 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------