%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET015-2 : TPTP v9.0.0. Bugfixed v2.1.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 : n013.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:37:29 PM UTC 2025
% Result : Unsatisfiable 12.32s 4.23s
% Output : CNFRefutation 12.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 11
% Syntax : Number of formulae : 38 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 69 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 57 ( 26 ~; 31 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 64 ( 64 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ subset > member > equal_sets > equal_elements > union > member_of_1_not_of_2 > intersection > #nlpp > complement > empty_set > ds > cs > bs > as
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(member_of_1_not_of_2,type,
member_of_1_not_of_2: ( $i * $i ) > $i ).
tff(ds,type,
ds: $i ).
tff(intersection,type,
intersection: ( $i * $i ) > $i ).
tff(union,type,
union: ( $i * $i ) > $i ).
tff(bs,type,
bs: $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff(complement,type,
complement: $i > $i ).
tff(member,type,
member: ( $i * $i ) > $o ).
tff(equal_elements,type,
equal_elements: ( $i * $i ) > $o ).
tff(empty_set,type,
empty_set: $i ).
tff(equal_sets,type,
equal_sets: ( $i * $i ) > $o ).
tff(as,type,
as: $i ).
tff(cs,type,
cs: $i ).
tff(f_170,axiom,
~ equal_sets(cs,ds),
file(unknown,unknown) ).
tff(f_61,axiom,
! [Subset,Superset] :
( subset(Subset,Superset)
| member(member_of_1_not_of_2(Subset,Superset),Subset) ),
file(unknown,unknown) ).
tff(f_95,axiom,
! [X,Xs,Ys] :
( ~ member(X,union(Xs,Ys))
| member(X,Xs)
| member(X,Ys) ),
file(unknown,unknown) ).
tff(f_83,axiom,
! [X,Xs,Ys] :
( ~ member(X,Xs)
| member(X,union(Xs,Ys)) ),
file(unknown,unknown) ).
tff(f_66,axiom,
! [Subset,Superset] :
( ~ member(member_of_1_not_of_2(Subset,Superset),Superset)
| subset(Subset,Superset) ),
file(unknown,unknown) ).
tff(f_88,axiom,
! [X,Ys,Xs] :
( ~ member(X,Ys)
| member(X,union(Xs,Ys)) ),
file(unknown,unknown) ).
tff(f_133,axiom,
! [Set1,Set2] :
( ~ subset(Set1,Set2)
| ~ subset(Set2,Set1)
| equal_sets(Set2,Set1) ),
file(unknown,unknown) ).
tff(f_168,axiom,
equal_sets(union(bs,as),ds),
file(unknown,unknown) ).
tff(f_149,axiom,
! [Xs,Ys,Zs] :
( ~ equal_sets(Xs,Ys)
| ~ equal_sets(Ys,Zs)
| equal_sets(Xs,Zs) ),
file(unknown,unknown) ).
tff(f_141,axiom,
! [Xs,Ys] :
( ~ equal_sets(Xs,Ys)
| equal_sets(Ys,Xs) ),
file(unknown,unknown) ).
tff(f_167,axiom,
equal_sets(union(as,bs),cs),
file(unknown,unknown) ).
tff(c_48,plain,
~ equal_sets(cs,ds),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_6,plain,
! [Subset_5,Superset_6] :
( member(member_of_1_not_of_2(Subset_5,Superset_6),Subset_5)
| subset(Subset_5,Superset_6) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_386,plain,
! [X_114,Ys_115,Xs_116] :
( member(X_114,Ys_115)
| member(X_114,Xs_116)
| ~ member(X_114,union(Xs_116,Ys_115)) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_1227,plain,
! [Xs_199,Ys_200,Superset_201] :
( member(member_of_1_not_of_2(union(Xs_199,Ys_200),Superset_201),Ys_200)
| member(member_of_1_not_of_2(union(Xs_199,Ys_200),Superset_201),Xs_199)
| subset(union(Xs_199,Ys_200),Superset_201) ),
inference(resolution,[status(thm)],[c_6,c_386]) ).
tff(c_114,plain,
! [X_73,Xs_74,Ys_75] :
( member(X_73,union(Xs_74,Ys_75))
| ~ member(X_73,Xs_74) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_8,plain,
! [Subset_7,Superset_8] :
( subset(Subset_7,Superset_8)
| ~ member(member_of_1_not_of_2(Subset_7,Superset_8),Superset_8) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_119,plain,
! [Subset_7,Xs_74,Ys_75] :
( subset(Subset_7,union(Xs_74,Ys_75))
| ~ member(member_of_1_not_of_2(Subset_7,union(Xs_74,Ys_75)),Xs_74) ),
inference(resolution,[status(thm)],[c_114,c_8]) ).
tff(c_9933,plain,
! [Xs_646,Ys_647,Ys_648] :
( member(member_of_1_not_of_2(union(Xs_646,Ys_647),union(Ys_647,Ys_648)),Xs_646)
| subset(union(Xs_646,Ys_647),union(Ys_647,Ys_648)) ),
inference(resolution,[status(thm)],[c_1227,c_119]) ).
tff(c_16,plain,
! [X_16,Xs_18,Ys_17] :
( member(X_16,union(Xs_18,Ys_17))
| ~ member(X_16,Ys_17) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_85,plain,
! [Subset_67,Superset_68] :
( subset(Subset_67,Superset_68)
| ~ member(member_of_1_not_of_2(Subset_67,Superset_68),Superset_68) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_94,plain,
! [Subset_67,Xs_18,Ys_17] :
( subset(Subset_67,union(Xs_18,Ys_17))
| ~ member(member_of_1_not_of_2(Subset_67,union(Xs_18,Ys_17)),Ys_17) ),
inference(resolution,[status(thm)],[c_16,c_85]) ).
tff(c_10014,plain,
! [Xs_646,Ys_647] : subset(union(Xs_646,Ys_647),union(Ys_647,Xs_646)),
inference(resolution,[status(thm)],[c_9933,c_94]) ).
tff(c_10026,plain,
! [Xs_649,Ys_650] : subset(union(Xs_649,Ys_650),union(Ys_650,Xs_649)),
inference(resolution,[status(thm)],[c_9933,c_94]) ).
tff(c_30,plain,
! [Set2_36,Set1_35] :
( equal_sets(Set2_36,Set1_35)
| ~ subset(Set2_36,Set1_35)
| ~ subset(Set1_35,Set2_36) ),
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_10030,plain,
! [Xs_649,Ys_650] :
( equal_sets(union(Xs_649,Ys_650),union(Ys_650,Xs_649))
| ~ subset(union(Ys_650,Xs_649),union(Xs_649,Ys_650)) ),
inference(resolution,[status(thm)],[c_10026,c_30]) ).
tff(c_10035,plain,
! [Xs_651,Ys_652] : equal_sets(union(Xs_651,Ys_652),union(Ys_652,Xs_651)),
inference(demodulation,[status(thm),theory(equality)],[c_10014,c_10030]) ).
tff(c_46,plain,
equal_sets(union(bs,as),ds),
inference(cnfTransformation,[status(thm)],[f_168]) ).
tff(c_132,plain,
! [Xs_82,Zs_83,Ys_84] :
( equal_sets(Xs_82,Zs_83)
| ~ equal_sets(Ys_84,Zs_83)
| ~ equal_sets(Xs_82,Ys_84) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_146,plain,
! [Xs_82] :
( equal_sets(Xs_82,ds)
| ~ equal_sets(Xs_82,union(bs,as)) ),
inference(resolution,[status(thm)],[c_46,c_132]) ).
tff(c_10070,plain,
equal_sets(union(as,bs),ds),
inference(resolution,[status(thm)],[c_10035,c_146]) ).
tff(c_34,plain,
! [Ys_39,Xs_38] :
( equal_sets(Ys_39,Xs_38)
| ~ equal_sets(Xs_38,Ys_39) ),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_10086,plain,
equal_sets(ds,union(as,bs)),
inference(resolution,[status(thm)],[c_10070,c_34]) ).
tff(c_44,plain,
equal_sets(union(as,bs),cs),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_145,plain,
! [Xs_82] :
( equal_sets(Xs_82,cs)
| ~ equal_sets(Xs_82,union(as,bs)) ),
inference(resolution,[status(thm)],[c_44,c_132]) ).
tff(c_10100,plain,
equal_sets(ds,cs),
inference(resolution,[status(thm)],[c_10086,c_145]) ).
tff(c_10107,plain,
equal_sets(cs,ds),
inference(resolution,[status(thm)],[c_10100,c_34]) ).
tff(c_10112,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48,c_10107]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SET015-2 : TPTP v9.0.0. Bugfixed v2.1.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.13/0.34 % Computer : n013.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 19:41:32 EDT 2025
% 0.13/0.35 % CPUTime :
% 12.32/4.23 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.32/4.24
% 12.32/4.24 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------