%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : CSR036+1 : TPTP v9.0.0. Released v3.4.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 : 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 05:53:32 PM UTC 2025
% Result : Theorem 16.13s 6.46s
% Output : CNFRefutation 16.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 34
% Syntax : Number of formulae : 140 ( 94 unt; 0 typ; 0 def)
% Number of atoms : 190 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 118 ( 68 ~; 44 |; 2 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 40 con; 0-0 aty)
% Number of variables : 51 ( 51 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ isa > genls > genlpreds > genlmt > genlinverse > disjointwith > transitivebinarypredicate > tptpcol_9_72709 > tptpcol_9_22021 > tptpcol_8_72708 > tptpcol_8_22020 > tptpcol_7_72707 > tptpcol_7_21508 > tptpcol_6_71683 > tptpcol_6_20484 > tptpcol_5_69635 > tptpcol_5_20483 > tptpcol_4_65539 > tptpcol_4_16387 > tptpcol_3_65538 > tptpcol_3_16386 > tptpcol_2_65537 > tptpcol_2_2 > tptpcol_1_65536 > tptpcol_1_1 > tptpcol_16_72795 > tptpcol_15_72793 > tptpcol_15_22076 > tptpcol_14_72792 > tptpcol_14_22072 > tptpcol_13_72791 > tptpcol_13_22071 > tptpcol_12_72775 > tptpcol_12_22055 > tptpcol_11_72774 > tptpcol_11_22023 > tptpcol_10_72710 > tptpcol_10_22022 > thing > predicate > mtvisible > microtheory > collection > binarypredicate > #nlpp > c_universalvocabularymt > c_transitivebinarypredicate > c_tptpcol_9_72709 > c_tptpcol_9_22021 > c_tptpcol_8_72708 > c_tptpcol_8_22020 > c_tptpcol_7_72707 > c_tptpcol_7_21508 > c_tptpcol_6_71683 > c_tptpcol_6_20484 > c_tptpcol_5_69635 > c_tptpcol_5_20483 > c_tptpcol_4_65539 > c_tptpcol_4_16387 > c_tptpcol_3_65538 > c_tptpcol_3_16386 > c_tptpcol_2_65537 > c_tptpcol_2_2 > c_tptpcol_1_65536 > c_tptpcol_1_1 > c_tptpcol_16_72795 > c_tptpcol_15_72793 > c_tptpcol_15_22076 > c_tptpcol_14_72792 > c_tptpcol_14_22072 > c_tptpcol_13_72791 > c_tptpcol_13_22071 > c_tptpcol_12_72775 > c_tptpcol_12_22055 > c_tptpcol_11_72774 > c_tptpcol_11_22023 > c_tptpcol_10_72710 > c_tptpcol_10_22022 > c_tptp_spindleheadmt > c_tptp_member974_mt > c_genlmt > c_cyclistsmt > c_calendarsvocabularymt > c_calendarsmt > c_basekb
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(c_tptpcol_6_20484,type,
c_tptpcol_6_20484: $i ).
tff(mtvisible,type,
mtvisible: $i > $o ).
tff(microtheory,type,
microtheory: $i > $o ).
tff(genls,type,
genls: ( $i * $i ) > $o ).
tff(tptpcol_7_72707,type,
tptpcol_7_72707: $i > $o ).
tff(tptpcol_5_20483,type,
tptpcol_5_20483: $i > $o ).
tff(genlpreds,type,
genlpreds: ( $i * $i ) > $o ).
tff(c_tptpcol_9_72709,type,
c_tptpcol_9_72709: $i ).
tff(collection,type,
collection: $i > $o ).
tff(tptpcol_1_1,type,
tptpcol_1_1: $i > $o ).
tff(tptpcol_5_69635,type,
tptpcol_5_69635: $i > $o ).
tff(tptpcol_12_22055,type,
tptpcol_12_22055: $i > $o ).
tff(c_tptpcol_2_65537,type,
c_tptpcol_2_65537: $i ).
tff(c_tptpcol_14_72792,type,
c_tptpcol_14_72792: $i ).
tff(binarypredicate,type,
binarypredicate: $i > $o ).
tff(tptpcol_6_71683,type,
tptpcol_6_71683: $i > $o ).
tff(c_tptpcol_4_16387,type,
c_tptpcol_4_16387: $i ).
tff(c_calendarsmt,type,
c_calendarsmt: $i ).
tff(genlmt,type,
genlmt: ( $i * $i ) > $o ).
tff(tptpcol_16_72795,type,
tptpcol_16_72795: $i > $o ).
tff(c_tptpcol_12_72775,type,
c_tptpcol_12_72775: $i ).
tff(tptpcol_2_65537,type,
tptpcol_2_65537: $i > $o ).
tff(c_genlmt,type,
c_genlmt: $i ).
tff(c_tptpcol_15_22076,type,
c_tptpcol_15_22076: $i ).
tff(c_tptpcol_4_65539,type,
c_tptpcol_4_65539: $i ).
tff(tptpcol_7_21508,type,
tptpcol_7_21508: $i > $o ).
tff(isa,type,
isa: ( $i * $i ) > $o ).
tff(c_tptpcol_11_22023,type,
c_tptpcol_11_22023: $i ).
tff(c_tptpcol_2_2,type,
c_tptpcol_2_2: $i ).
tff(c_tptpcol_3_65538,type,
c_tptpcol_3_65538: $i ).
tff(tptpcol_12_72775,type,
tptpcol_12_72775: $i > $o ).
tff(c_transitivebinarypredicate,type,
c_transitivebinarypredicate: $i ).
tff(c_tptpcol_5_20483,type,
c_tptpcol_5_20483: $i ).
tff(c_tptpcol_7_21508,type,
c_tptpcol_7_21508: $i ).
tff(predicate,type,
predicate: $i > $o ).
tff(c_tptpcol_10_72710,type,
c_tptpcol_10_72710: $i ).
tff(tptpcol_11_72774,type,
tptpcol_11_72774: $i > $o ).
tff(c_cyclistsmt,type,
c_cyclistsmt: $i ).
tff(c_calendarsvocabularymt,type,
c_calendarsvocabularymt: $i ).
tff(disjointwith,type,
disjointwith: ( $i * $i ) > $o ).
tff(tptpcol_15_22076,type,
tptpcol_15_22076: $i > $o ).
tff(c_tptpcol_7_72707,type,
c_tptpcol_7_72707: $i ).
tff(tptpcol_11_22023,type,
tptpcol_11_22023: $i > $o ).
tff(tptpcol_14_22072,type,
tptpcol_14_22072: $i > $o ).
tff(c_tptpcol_10_22022,type,
c_tptpcol_10_22022: $i ).
tff(thing,type,
thing: $i > $o ).
tff(tptpcol_13_72791,type,
tptpcol_13_72791: $i > $o ).
tff(c_tptpcol_13_72791,type,
c_tptpcol_13_72791: $i ).
tff(c_tptpcol_15_72793,type,
c_tptpcol_15_72793: $i ).
tff(tptpcol_10_22022,type,
tptpcol_10_22022: $i > $o ).
tff(tptpcol_8_22020,type,
tptpcol_8_22020: $i > $o ).
tff(tptpcol_10_72710,type,
tptpcol_10_72710: $i > $o ).
tff(tptpcol_1_65536,type,
tptpcol_1_65536: $i > $o ).
tff(tptpcol_6_20484,type,
tptpcol_6_20484: $i > $o ).
tff(tptpcol_9_22021,type,
tptpcol_9_22021: $i > $o ).
tff(tptpcol_8_72708,type,
tptpcol_8_72708: $i > $o ).
tff(c_tptp_spindleheadmt,type,
c_tptp_spindleheadmt: $i ).
tff(c_basekb,type,
c_basekb: $i ).
tff(c_tptpcol_14_22072,type,
c_tptpcol_14_22072: $i ).
tff(tptpcol_14_72792,type,
tptpcol_14_72792: $i > $o ).
tff(c_tptpcol_13_22071,type,
c_tptpcol_13_22071: $i ).
tff(c_tptpcol_16_72795,type,
c_tptpcol_16_72795: $i ).
tff(c_tptpcol_6_71683,type,
c_tptpcol_6_71683: $i ).
tff(c_tptpcol_12_22055,type,
c_tptpcol_12_22055: $i ).
tff(c_universalvocabularymt,type,
c_universalvocabularymt: $i ).
tff(c_tptpcol_1_1,type,
c_tptpcol_1_1: $i ).
tff(tptpcol_13_22071,type,
tptpcol_13_22071: $i > $o ).
tff(transitivebinarypredicate,type,
transitivebinarypredicate: $i > $o ).
tff(tptpcol_9_72709,type,
tptpcol_9_72709: $i > $o ).
tff(tptpcol_3_16386,type,
tptpcol_3_16386: $i > $o ).
tff(c_tptpcol_5_69635,type,
c_tptpcol_5_69635: $i ).
tff(c_tptpcol_9_22021,type,
c_tptpcol_9_22021: $i ).
tff(c_tptpcol_8_72708,type,
c_tptpcol_8_72708: $i ).
tff(tptpcol_3_65538,type,
tptpcol_3_65538: $i > $o ).
tff(c_tptpcol_3_16386,type,
c_tptpcol_3_16386: $i ).
tff(genlinverse,type,
genlinverse: ( $i * $i ) > $o ).
tff(c_tptpcol_1_65536,type,
c_tptpcol_1_65536: $i ).
tff(tptpcol_15_72793,type,
tptpcol_15_72793: $i > $o ).
tff(c_tptpcol_11_72774,type,
c_tptpcol_11_72774: $i ).
tff(tptpcol_4_65539,type,
tptpcol_4_65539: $i > $o ).
tff(c_tptpcol_8_22020,type,
c_tptpcol_8_22020: $i ).
tff(tptpcol_2_2,type,
tptpcol_2_2: $i > $o ).
tff(c_tptp_member974_mt,type,
c_tptp_member974_mt: $i ).
tff(tptpcol_4_16387,type,
tptpcol_4_16387: $i > $o ).
tff(f_99,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just24) ).
tff(f_320,axiom,
! [OLD,ARG2,NEW] :
( ( disjointwith(OLD,ARG2)
& genls(NEW,OLD) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just85) ).
tff(f_105,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just26) ).
tff(f_111,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just28) ).
tff(f_117,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
tff(f_123,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just32) ).
tff(f_719,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query36) ).
tff(f_219,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just64) ).
tff(f_308,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just83) ).
tff(f_129,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just34) ).
tff(f_45,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just6) ).
tff(f_314,axiom,
! [ARG1,OLD,NEW] :
( ( disjointwith(ARG1,OLD)
& genls(NEW,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just84) ).
tff(f_135,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just36) ).
tff(f_141,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just38) ).
tff(f_147,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
tff(f_57,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
tff(f_63,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just12) ).
tff(f_159,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
tff(f_165,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just46) ).
tff(f_171,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just48) ).
tff(f_69,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just14) ).
tff(f_177,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just50) ).
tff(f_51,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just8) ).
tff(f_153,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just42) ).
tff(f_183,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just52) ).
tff(f_189,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just54) ).
tff(f_81,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just18) ).
tff(f_87,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just20) ).
tff(f_201,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just58) ).
tff(f_207,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just60) ).
tff(f_213,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just62) ).
tff(f_93,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
tff(f_195,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just56) ).
tff(f_75,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just16) ).
tff(c_48,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_2038,plain,
! [NEW_392,ARG2_393,OLD_394] :
( disjointwith(NEW_392,ARG2_393)
| ~ genls(NEW_392,OLD_394)
| ~ disjointwith(OLD_394,ARG2_393) ),
inference(cnfTransformation,[status(thm)],[f_320]) ).
tff(c_2120,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_11_22023,ARG2_393)
| ~ disjointwith(c_tptpcol_10_22022,ARG2_393) ),
inference(resolution,[status(thm)],[c_48,c_2038]) ).
tff(c_52,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_2121,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_12_22055,ARG2_393)
| ~ disjointwith(c_tptpcol_11_22023,ARG2_393) ),
inference(resolution,[status(thm)],[c_52,c_2038]) ).
tff(c_56,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_8050,plain,
! [ARG2_645] :
( disjointwith(c_tptpcol_13_22071,ARG2_645)
| ~ disjointwith(c_tptpcol_12_22055,ARG2_645) ),
inference(resolution,[status(thm)],[c_56,c_2038]) ).
tff(c_60,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_2125,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_14_22072,ARG2_393)
| ~ disjointwith(c_tptpcol_13_22071,ARG2_393) ),
inference(resolution,[status(thm)],[c_60,c_2038]) ).
tff(c_64,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_2515,plain,
! [ARG2_419] :
( disjointwith(c_tptpcol_15_22076,ARG2_419)
| ~ disjointwith(c_tptpcol_14_22072,ARG2_419) ),
inference(resolution,[status(thm)],[c_64,c_2038]) ).
tff(c_348,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnfTransformation,[status(thm)],[f_719]) ).
tff(c_2543,plain,
~ disjointwith(c_tptpcol_14_22072,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_2515,c_348]) ).
tff(c_2550,plain,
~ disjointwith(c_tptpcol_13_22071,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_2125,c_2543]) ).
tff(c_8099,plain,
~ disjointwith(c_tptpcol_12_22055,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_8050,c_2550]) ).
tff(c_8136,plain,
~ disjointwith(c_tptpcol_11_22023,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_2121,c_8099]) ).
tff(c_8198,plain,
~ disjointwith(c_tptpcol_10_22022,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_2120,c_8136]) ).
tff(c_128,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnfTransformation,[status(thm)],[f_219]) ).
tff(c_1424,plain,
! [Y_352,X_353] :
( disjointwith(Y_352,X_353)
| ~ disjointwith(X_353,Y_352) ),
inference(cnfTransformation,[status(thm)],[f_308]) ).
tff(c_1427,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolution,[status(thm)],[c_128,c_1424]) ).
tff(c_68,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_2128,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_2_65537,ARG2_393)
| ~ disjointwith(c_tptpcol_1_65536,ARG2_393) ),
inference(resolution,[status(thm)],[c_68,c_2038]) ).
tff(c_12,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_1522,plain,
! [ARG1_360,NEW_361,OLD_362] :
( disjointwith(ARG1_360,NEW_361)
| ~ genls(NEW_361,OLD_362)
| ~ disjointwith(ARG1_360,OLD_362) ),
inference(cnfTransformation,[status(thm)],[f_314]) ).
tff(c_5104,plain,
! [ARG1_549] :
( disjointwith(ARG1_549,c_tptpcol_2_2)
| ~ disjointwith(ARG1_549,c_tptpcol_1_1) ),
inference(resolution,[status(thm)],[c_12,c_1522]) ).
tff(c_166,plain,
! [Y_65,X_64] :
( disjointwith(Y_65,X_64)
| ~ disjointwith(X_64,Y_65) ),
inference(cnfTransformation,[status(thm)],[f_308]) ).
tff(c_9659,plain,
! [ARG1_658] :
( disjointwith(c_tptpcol_2_2,ARG1_658)
| ~ disjointwith(ARG1_658,c_tptpcol_1_1) ),
inference(resolution,[status(thm)],[c_5104,c_166]) ).
tff(c_9740,plain,
( disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537)
| ~ disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1) ),
inference(resolution,[status(thm)],[c_2128,c_9659]) ).
tff(c_9787,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(demodulation,[status(thm),theory(equality)],[c_1427,c_9740]) ).
tff(c_9800,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2),
inference(resolution,[status(thm)],[c_9787,c_166]) ).
tff(c_72,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_3790,plain,
! [ARG2_489] :
( disjointwith(c_tptpcol_3_65538,ARG2_489)
| ~ disjointwith(c_tptpcol_2_65537,ARG2_489) ),
inference(resolution,[status(thm)],[c_72,c_2038]) ).
tff(c_3812,plain,
! [ARG2_489] :
( disjointwith(ARG2_489,c_tptpcol_3_65538)
| ~ disjointwith(c_tptpcol_2_65537,ARG2_489) ),
inference(resolution,[status(thm)],[c_3790,c_166]) ).
tff(c_9911,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_3_65538),
inference(resolution,[status(thm)],[c_9800,c_3812]) ).
tff(c_10366,plain,
disjointwith(c_tptpcol_3_65538,c_tptpcol_2_2),
inference(resolution,[status(thm)],[c_9911,c_166]) ).
tff(c_76,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_2103,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_4_65539,ARG2_393)
| ~ disjointwith(c_tptpcol_3_65538,ARG2_393) ),
inference(resolution,[status(thm)],[c_76,c_2038]) ).
tff(c_80,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_2102,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_5_69635,ARG2_393)
| ~ disjointwith(c_tptpcol_4_65539,ARG2_393) ),
inference(resolution,[status(thm)],[c_80,c_2038]) ).
tff(c_20,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2111,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_4_16387,ARG2_393)
| ~ disjointwith(c_tptpcol_3_16386,ARG2_393) ),
inference(resolution,[status(thm)],[c_20,c_2038]) ).
tff(c_24,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_2110,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_5_20483,ARG2_393)
| ~ disjointwith(c_tptpcol_4_16387,ARG2_393) ),
inference(resolution,[status(thm)],[c_24,c_2038]) ).
tff(c_88,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_1584,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_7_72707)
| ~ disjointwith(ARG1_360,c_tptpcol_6_71683) ),
inference(resolution,[status(thm)],[c_88,c_1522]) ).
tff(c_92,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_1589,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_8_72708)
| ~ disjointwith(ARG1_360,c_tptpcol_7_72707) ),
inference(resolution,[status(thm)],[c_92,c_1522]) ).
tff(c_96,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_1611,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_9_72709)
| ~ disjointwith(ARG1_360,c_tptpcol_8_72708) ),
inference(resolution,[status(thm)],[c_96,c_1522]) ).
tff(c_28,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_3880,plain,
! [ARG2_495] :
( disjointwith(c_tptpcol_6_20484,ARG2_495)
| ~ disjointwith(c_tptpcol_5_20483,ARG2_495) ),
inference(resolution,[status(thm)],[c_28,c_2038]) ).
tff(c_100,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnfTransformation,[status(thm)],[f_177]) ).
tff(c_1610,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_10_72710)
| ~ disjointwith(ARG1_360,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[c_100,c_1522]) ).
tff(c_3899,plain,
( disjointwith(c_tptpcol_6_20484,c_tptpcol_10_72710)
| ~ disjointwith(c_tptpcol_5_20483,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[c_3880,c_1610]) ).
tff(c_8509,plain,
~ disjointwith(c_tptpcol_5_20483,c_tptpcol_9_72709),
inference(splitLeft,[status(thm)],[c_3899]) ).
tff(c_8517,plain,
~ disjointwith(c_tptpcol_5_20483,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[c_1611,c_8509]) ).
tff(c_8532,plain,
~ disjointwith(c_tptpcol_5_20483,c_tptpcol_7_72707),
inference(resolution,[status(thm)],[c_1589,c_8517]) ).
tff(c_8557,plain,
~ disjointwith(c_tptpcol_5_20483,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[c_1584,c_8532]) ).
tff(c_8657,plain,
~ disjointwith(c_tptpcol_4_16387,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[c_2110,c_8557]) ).
tff(c_8777,plain,
~ disjointwith(c_tptpcol_3_16386,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[c_2111,c_8657]) ).
tff(c_16,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_1592,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_3_16386)
| ~ disjointwith(ARG1_360,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[c_16,c_1522]) ).
tff(c_84,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_3508,plain,
! [ARG2_478] :
( disjointwith(c_tptpcol_6_71683,ARG2_478)
| ~ disjointwith(c_tptpcol_5_69635,ARG2_478) ),
inference(resolution,[status(thm)],[c_84,c_2038]) ).
tff(c_10805,plain,
! [ARG2_664] :
( disjointwith(ARG2_664,c_tptpcol_6_71683)
| ~ disjointwith(c_tptpcol_5_69635,ARG2_664) ),
inference(resolution,[status(thm)],[c_3508,c_166]) ).
tff(c_10834,plain,
( disjointwith(c_tptpcol_3_16386,c_tptpcol_6_71683)
| ~ disjointwith(c_tptpcol_5_69635,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[c_1592,c_10805]) ).
tff(c_10904,plain,
~ disjointwith(c_tptpcol_5_69635,c_tptpcol_2_2),
inference(negUnitSimplification,[status(thm)],[c_8777,c_10834]) ).
tff(c_11008,plain,
~ disjointwith(c_tptpcol_4_65539,c_tptpcol_2_2),
inference(resolution,[status(thm)],[c_2102,c_10904]) ).
tff(c_11023,plain,
~ disjointwith(c_tptpcol_3_65538,c_tptpcol_2_2),
inference(resolution,[status(thm)],[c_2103,c_11008]) ).
tff(c_11030,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10366,c_11023]) ).
tff(c_11031,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_10_72710),
inference(splitRight,[status(thm)],[c_3899]) ).
tff(c_104,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_1590,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_11_72774)
| ~ disjointwith(ARG1_360,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[c_104,c_1522]) ).
tff(c_108,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_1602,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_12_72775)
| ~ disjointwith(ARG1_360,c_tptpcol_11_72774) ),
inference(resolution,[status(thm)],[c_108,c_1522]) ).
tff(c_36,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_1598,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_8_22020)
| ~ disjointwith(ARG1_360,c_tptpcol_7_21508) ),
inference(resolution,[status(thm)],[c_36,c_1522]) ).
tff(c_40,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_1603,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_9_22021)
| ~ disjointwith(ARG1_360,c_tptpcol_8_22020) ),
inference(resolution,[status(thm)],[c_40,c_1522]) ).
tff(c_116,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_2116,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_14_72792,ARG2_393)
| ~ disjointwith(c_tptpcol_13_72791,ARG2_393) ),
inference(resolution,[status(thm)],[c_116,c_2038]) ).
tff(c_120,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_2115,plain,
! [ARG2_393] :
( disjointwith(c_tptpcol_15_72793,ARG2_393)
| ~ disjointwith(c_tptpcol_14_72792,ARG2_393) ),
inference(resolution,[status(thm)],[c_120,c_2038]) ).
tff(c_124,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_3587,plain,
! [ARG2_482] :
( disjointwith(c_tptpcol_16_72795,ARG2_482)
| ~ disjointwith(c_tptpcol_15_72793,ARG2_482) ),
inference(resolution,[status(thm)],[c_124,c_2038]) ).
tff(c_44,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_1601,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_10_22022)
| ~ disjointwith(ARG1_360,c_tptpcol_9_22021) ),
inference(resolution,[status(thm)],[c_44,c_1522]) ).
tff(c_3607,plain,
( disjointwith(c_tptpcol_16_72795,c_tptpcol_10_22022)
| ~ disjointwith(c_tptpcol_15_72793,c_tptpcol_9_22021) ),
inference(resolution,[status(thm)],[c_3587,c_1601]) ).
tff(c_11318,plain,
~ disjointwith(c_tptpcol_15_72793,c_tptpcol_9_22021),
inference(splitLeft,[status(thm)],[c_3607]) ).
tff(c_11325,plain,
~ disjointwith(c_tptpcol_14_72792,c_tptpcol_9_22021),
inference(resolution,[status(thm)],[c_2115,c_11318]) ).
tff(c_11334,plain,
~ disjointwith(c_tptpcol_13_72791,c_tptpcol_9_22021),
inference(resolution,[status(thm)],[c_2116,c_11325]) ).
tff(c_11366,plain,
~ disjointwith(c_tptpcol_13_72791,c_tptpcol_8_22020),
inference(resolution,[status(thm)],[c_1603,c_11334]) ).
tff(c_11517,plain,
~ disjointwith(c_tptpcol_13_72791,c_tptpcol_7_21508),
inference(resolution,[status(thm)],[c_1598,c_11366]) ).
tff(c_112,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_1606,plain,
! [ARG1_360] :
( disjointwith(ARG1_360,c_tptpcol_13_72791)
| ~ disjointwith(ARG1_360,c_tptpcol_12_72775) ),
inference(resolution,[status(thm)],[c_112,c_1522]) ).
tff(c_32,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_5167,plain,
! [ARG2_553] :
( disjointwith(c_tptpcol_7_21508,ARG2_553)
| ~ disjointwith(c_tptpcol_6_20484,ARG2_553) ),
inference(resolution,[status(thm)],[c_32,c_2038]) ).
tff(c_12010,plain,
! [ARG2_670] :
( disjointwith(ARG2_670,c_tptpcol_7_21508)
| ~ disjointwith(c_tptpcol_6_20484,ARG2_670) ),
inference(resolution,[status(thm)],[c_5167,c_166]) ).
tff(c_12085,plain,
( disjointwith(c_tptpcol_13_72791,c_tptpcol_7_21508)
| ~ disjointwith(c_tptpcol_6_20484,c_tptpcol_12_72775) ),
inference(resolution,[status(thm)],[c_1606,c_12010]) ).
tff(c_12132,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_12_72775),
inference(negUnitSimplification,[status(thm)],[c_11517,c_12085]) ).
tff(c_12191,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_11_72774),
inference(resolution,[status(thm)],[c_1602,c_12132]) ).
tff(c_12493,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[c_1590,c_12191]) ).
tff(c_12500,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_11031,c_12493]) ).
tff(c_12501,plain,
disjointwith(c_tptpcol_16_72795,c_tptpcol_10_22022),
inference(splitRight,[status(thm)],[c_3607]) ).
tff(c_12506,plain,
disjointwith(c_tptpcol_10_22022,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[c_12501,c_166]) ).
tff(c_12517,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8198,c_12506]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : CSR036+1 : TPTP v9.0.0. Released v3.4.0.
% 0.12/0.14 % 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.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Mon Apr 7 16:43:33 EDT 2025
% 0.13/0.36 % CPUTime :
% 16.13/6.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.13/6.47
% 16.13/6.47 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------