%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX228-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/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 : n008.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:39 PM UTC 2026
% Result : Unsatisfiable 17.01s 6.21s
% Output : CNFRefutation 17.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 37 ( 34 unt; 0 typ; 0 def)
% Number of atoms : 40 ( 39 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 7 ~; 3 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 15 ( 15 usr; 4 con; 0-4 aty)
% Number of variables : 60 ( 60 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ aux > union > prop_union_comm > eqNat > eq3 > eq2 > eq > elem > cons > barbar > #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(prop_union_comm,type,
prop_union_comm: ( $i * $i ) > $i ).
tff(eqNat,type,
eqNat: ( $i * $i ) > $i ).
tff(s,type,
s: $i > $i ).
tff(elem,type,
elem: ( $i * $i ) > $i ).
tff(union,type,
union: ( $i * $i ) > $i ).
tff(aux,type,
aux: ( $i * $i * $i * $i ) > $i ).
tff(barbar,type,
barbar: ( $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_58,axiom,
! [X] : ( eq2(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [X] : ( eq3(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_74,axiom,
! [X,Y] : ( eq(cons(X,Y),nil) = bfalse ),
file(unknown,unknown) ).
tff(f_70,axiom,
! [X,Z,Y,X2] :
( ( eq2(X,Z) != btrue )
| ( eq(cons(X,Y),cons(Z,X2)) = eq(Y,X2) ) ),
file(unknown,unknown) ).
tff(f_42,axiom,
! [Y] : ( union(nil,Y) = Y ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [Y,Z,Xs] : ( aux(Y,Z,Xs,btrue) = union(Xs,Y) ),
file(unknown,unknown) ).
tff(f_27,axiom,
! [Y] : ( barbar(btrue,Y) = btrue ),
file(unknown,unknown) ).
tff(f_36,axiom,
eqNat(z,z) = btrue,
file(unknown,unknown) ).
tff(f_40,axiom,
! [X,Z,Xs] : ( elem(X,cons(Z,Xs)) = barbar(eqNat(X,Z),elem(X,Xs)) ),
file(unknown,unknown) ).
tff(f_44,axiom,
! [Z,Xs,Y] : ( union(cons(Z,Xs),Y) = aux(Y,Z,Xs,elem(Z,Y)) ),
file(unknown,unknown) ).
tff(f_46,axiom,
! [X,Y] : ( prop_union_comm(X,Y) = eq(union(X,Y),union(Y,X)) ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [X,Y] : ( eq3(prop_union_comm(X,Y),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_40,plain,
! [X_28] : ( eq2(X_28,X_28) = btrue ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_42,plain,
! [X_29] : ( eq3(X_29,X_29) = btrue ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_50,plain,
! [X_40,Y_41] : ( eq(cons(X_40,Y_41),nil) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_46,plain,
! [X_34,Y_36,Z_35,X2_37] :
( ( eq(cons(X_34,Y_36),cons(Z_35,X2_37)) = eq(Y_36,X2_37) )
| ( eq2(X_34,Z_35) != btrue ) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_22,plain,
! [Y_17] : ( union(nil,Y_17) = Y_17 ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_2,plain,
! [Y_1,Z_2,Xs_3] : ( aux(Y_1,Z_2,Xs_3,btrue) = union(Xs_3,Y_1) ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_6,plain,
! [Y_7] : ( barbar(btrue,Y_7) = btrue ),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_16,plain,
eqNat(z,z) = btrue,
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_373,plain,
! [X_93,Z_94,Xs_95] : ( barbar(eqNat(X_93,Z_94),elem(X_93,Xs_95)) = elem(X_93,cons(Z_94,Xs_95)) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_391,plain,
! [Xs_95] : ( elem(z,cons(z,Xs_95)) = barbar(btrue,elem(z,Xs_95)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_373]) ).
tff(c_400,plain,
! [Xs_96] : ( elem(z,cons(z,Xs_96)) = btrue ),
inference(demodulation,[status(thm),theory(equality)],[c_6,c_391]) ).
tff(c_24,plain,
! [Y_20,Z_18,Xs_19] : ( aux(Y_20,Z_18,Xs_19,elem(Z_18,Y_20)) = union(cons(Z_18,Xs_19),Y_20) ),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_408,plain,
! [Xs_19,Xs_96] : ( union(cons(z,Xs_19),cons(z,Xs_96)) = aux(cons(z,Xs_96),z,Xs_19,btrue) ),
inference(superposition,[status(thm),theory(equality)],[c_400,c_24]) ).
tff(c_416,plain,
! [Xs_19,Xs_96] : ( union(cons(z,Xs_19),cons(z,Xs_96)) = union(Xs_19,cons(z,Xs_96)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_408]) ).
tff(c_615,plain,
! [Xs_113,Xs_114] : ( union(cons(z,Xs_113),cons(z,Xs_114)) = union(Xs_113,cons(z,Xs_114)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_408]) ).
tff(c_26,plain,
! [X_21,Y_22] : ( eq(union(X_21,Y_22),union(Y_22,X_21)) = prop_union_comm(X_21,Y_22) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_624,plain,
! [Xs_113,Xs_114] : ( eq(union(Xs_113,cons(z,Xs_114)),union(cons(z,Xs_114),cons(z,Xs_113))) = prop_union_comm(cons(z,Xs_113),cons(z,Xs_114)) ),
inference(superposition,[status(thm),theory(equality)],[c_615,c_26]) ).
tff(c_3752,plain,
! [Xs_321,Xs_322] : ( eq(union(Xs_321,cons(z,Xs_322)),union(Xs_322,cons(z,Xs_321))) = prop_union_comm(cons(z,Xs_321),cons(z,Xs_322)) ),
inference(demodulation,[status(thm),theory(equality)],[c_416,c_624]) ).
tff(c_3809,plain,
! [Xs_323] : ( eq(cons(z,Xs_323),union(Xs_323,cons(z,nil))) = prop_union_comm(cons(z,nil),cons(z,Xs_323)) ),
inference(superposition,[status(thm),theory(equality)],[c_22,c_3752]) ).
tff(c_23774,plain,
! [Xs_857] : ( eq(cons(z,cons(z,Xs_857)),union(Xs_857,cons(z,nil))) = prop_union_comm(cons(z,nil),cons(z,cons(z,Xs_857))) ),
inference(superposition,[status(thm),theory(equality)],[c_416,c_3809]) ).
tff(c_23803,plain,
prop_union_comm(cons(z,nil),cons(z,cons(z,nil))) = eq(cons(z,cons(z,nil)),cons(z,nil)),
inference(superposition,[status(thm),theory(equality)],[c_22,c_23774]) ).
tff(c_52,plain,
! [X_42,Y_43] : ( eq3(prop_union_comm(X_42,Y_43),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_23810,plain,
eq3(eq(cons(z,cons(z,nil)),cons(z,nil)),bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_23803,c_52]) ).
tff(c_23816,plain,
( ( eq3(eq(cons(z,nil),nil),bfalse) != btrue )
| ( eq2(z,z) != btrue ) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_23810]) ).
tff(c_23822,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_40,c_42,c_50,c_23816]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX228-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/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.15/0.33 % Computer : n008.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % 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 12:56:28 EDT 2026
% 0.15/0.34 % CPUTime :
% 17.01/6.21 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.01/6.22
% 17.01/6.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------