%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX200-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 : n015.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:35 PM UTC 2026
% Result : Unsatisfiable 4.64s 2.72s
% Output : CNFRefutation 4.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 39 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 39 ( 38 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 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-5 aty)
% Number of variables : 72 ( 72 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ aux > aux2 > prop_merge_ord_not3 > merge > leqNat > impl > eq2 > eq > cons > #nlpp > s > ord > z > nil > btrue > bfalse
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(eq,type,
eq: ( $i * $i ) > $i ).
tff(aux2,type,
aux2: ( $i * $i * $i * $i ) > $i ).
tff(ord,type,
ord: $i > $i ).
tff(s,type,
s: $i > $i ).
tff(leqNat,type,
leqNat: ( $i * $i ) > $i ).
tff(merge,type,
merge: ( $i * $i ) > $i ).
tff(impl,type,
impl: ( $i * $i ) > $i ).
tff(prop_merge_ord_not3,type,
prop_merge_ord_not3: ( $i * $i ) > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(aux,type,
aux: ( $i * $i * $i * $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_64,axiom,
! [X] : ( eq2(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_53,axiom,
eq2(bfalse,btrue) = bfalse,
file(unknown,unknown) ).
tff(f_39,axiom,
! [Z,Xs] : ( merge(cons(Z,Xs),nil) = cons(Z,Xs) ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [Z,Xs,Y2,Ys] : ( aux(Z,Xs,Y2,Ys,bfalse) = cons(Y2,merge(cons(Z,Xs),Ys)) ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [Y] : ( merge(nil,Y) = Y ),
file(unknown,unknown) ).
tff(f_23,axiom,
! [Z,Xs,Y2,Ys] : ( aux(Z,Xs,Y2,Ys,btrue) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
file(unknown,unknown) ).
tff(f_29,axiom,
! [Y,Y2,Xs] : ( aux2(Y,Y2,Xs,bfalse) = bfalse ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [Z] : ( leqNat(s(Z),z) = bfalse ),
file(unknown,unknown) ).
tff(f_46,axiom,
! [Y,Y2,Xs] : ( ord(cons(Y,cons(Y2,Xs))) = aux2(Y,Y2,Xs,leqNat(Y,Y2)) ),
file(unknown,unknown) ).
tff(f_48,axiom,
! [Q] : ( impl(btrue,Q) = Q ),
file(unknown,unknown) ).
tff(f_42,axiom,
ord(nil) = btrue,
file(unknown,unknown) ).
tff(f_52,axiom,
! [X,Y] : ( prop_merge_ord_not3(X,Y) = impl(eq2(ord(X),btrue),impl(eq2(ord(Y),bfalse),eq2(ord(merge(X,Y)),btrue))) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X,Y] : ( eq2(prop_merge_ord_not3(X,Y),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_46,plain,
! [X_39] : ( eq2(X_39,X_39) = btrue ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_34,plain,
eq2(bfalse,btrue) = bfalse,
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_18,plain,
! [Z_20,Xs_21] : ( merge(cons(Z_20,Xs_21),nil) = cons(Z_20,Xs_21) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_362,plain,
! [Y2_86,Z_87,Xs_88,Ys_89] : ( cons(Y2_86,merge(cons(Z_87,Xs_88),Ys_89)) = aux(Z_87,Xs_88,Y2_86,Ys_89,bfalse) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_457,plain,
! [Y2_94,Z_95,Xs_96] : ( cons(Y2_94,cons(Z_95,Xs_96)) = aux(Z_95,Xs_96,Y2_94,nil,bfalse) ),
inference(superposition,[status(thm),theory(equality)],[c_18,c_362]) ).
tff(c_16,plain,
! [Y_19] : ( merge(nil,Y_19) = Y_19 ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_202,plain,
! [Z_66,Xs_67,Y2_68,Ys_69] : ( cons(Z_66,merge(Xs_67,cons(Y2_68,Ys_69))) = aux(Z_66,Xs_67,Y2_68,Ys_69,btrue) ),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_224,plain,
! [Z_66,Y2_68,Ys_69] : ( cons(Z_66,cons(Y2_68,Ys_69)) = aux(Z_66,nil,Y2_68,Ys_69,btrue) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_202]) ).
tff(c_478,plain,
! [Z_95,Xs_96,Y2_94] : ( aux(Z_95,Xs_96,Y2_94,nil,bfalse) = aux(Y2_94,nil,Z_95,Xs_96,btrue) ),
inference(superposition,[status(thm),theory(equality)],[c_457,c_224]) ).
tff(c_8,plain,
! [Y_12,Y2_13,Xs_14] : ( aux2(Y_12,Y2_13,Xs_14,bfalse) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_12,plain,
! [Z_16] : ( leqNat(s(Z_16),z) = bfalse ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_26,plain,
! [Y_27,Y2_28,Xs_29] : ( ord(cons(Y_27,cons(Y2_28,Xs_29))) = aux2(Y_27,Y2_28,Xs_29,leqNat(Y_27,Y2_28)) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_329,plain,
! [Y_79,Y2_80,Xs_81] : ( aux2(Y_79,Y2_80,Xs_81,leqNat(Y_79,Y2_80)) = ord(aux(Y_79,nil,Y2_80,Xs_81,btrue)) ),
inference(demodulation,[status(thm),theory(equality)],[c_224,c_26]) ).
tff(c_341,plain,
! [Z_16,Xs_81] : ( ord(aux(s(Z_16),nil,z,Xs_81,btrue)) = aux2(s(Z_16),z,Xs_81,bfalse) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_329]) ).
tff(c_347,plain,
! [Z_16,Xs_81] : ( ord(aux(s(Z_16),nil,z,Xs_81,btrue)) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_341]) ).
tff(c_509,plain,
! [Xs_81,Z_16] : ( ord(aux(z,Xs_81,s(Z_16),nil,bfalse)) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_478,c_347]) ).
tff(c_28,plain,
! [Q_30] : ( impl(btrue,Q_30) = Q_30 ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_22,plain,
ord(nil) = btrue,
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_550,plain,
! [X_104,Y_105] : ( impl(eq2(ord(X_104),btrue),impl(eq2(ord(Y_105),bfalse),eq2(ord(merge(X_104,Y_105)),btrue))) = prop_merge_ord_not3(X_104,Y_105) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_595,plain,
! [Y_19] : ( impl(eq2(ord(nil),btrue),impl(eq2(ord(Y_19),bfalse),eq2(ord(Y_19),btrue))) = prop_merge_ord_not3(nil,Y_19) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_550]) ).
tff(c_757,plain,
! [Y_118] : ( impl(eq2(ord(Y_118),bfalse),eq2(ord(Y_118),btrue)) = prop_merge_ord_not3(nil,Y_118) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_46,c_22,c_595]) ).
tff(c_772,plain,
! [Xs_81,Z_16] : ( impl(eq2(bfalse,bfalse),eq2(ord(aux(z,Xs_81,s(Z_16),nil,bfalse)),btrue)) = prop_merge_ord_not3(nil,aux(z,Xs_81,s(Z_16),nil,bfalse)) ),
inference(superposition,[status(thm),theory(equality)],[c_509,c_757]) ).
tff(c_813,plain,
! [Xs_119,Z_120] : ( prop_merge_ord_not3(nil,aux(z,Xs_119,s(Z_120),nil,bfalse)) = bfalse ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_509,c_28,c_46,c_772]) ).
tff(c_48,plain,
! [X_40,Y_41] : ( eq2(prop_merge_ord_not3(X_40,Y_41),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_817,plain,
eq2(bfalse,bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_813,c_48]) ).
tff(c_823,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_46,c_817]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SWX200-1 : TPTP v9.3.0. Released v9.3.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.11/0.30 % Computer : n015.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Tue May 5 11:16:01 EDT 2026
% 0.11/0.30 % CPUTime :
% 4.64/2.72 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.64/2.73
% 4.64/2.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------