%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN717-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 : Thu May 9 17:48:43 EDT 2024
% Result : Unsatisfiable 0.70s 0.89s
% Output : Refutation 0.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 12
% Syntax : Number of clauses : 24 ( 13 unt; 0 nHn; 18 RR)
% Number of literals : 42 ( 0 equ; 21 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 36 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p24_26,negated_conjecture,
p24(X27,X27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_26) ).
cnf(p24_71,negated_conjecture,
( p24(X235,X234)
| ~ p24(X236,X235)
| ~ p24(X236,X234) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_71) ).
cnf(c77,plain,
( p24(X242,X243)
| ~ p24(X243,X242) ),
inference(resolution,[status(thm)],[p24_71,p24_26]) ).
cnf(p22_28,negated_conjecture,
p22(X29,X29),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p22_28) ).
cnf(p23_36,negated_conjecture,
p23(c79,c77),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_36) ).
cnf(p23_27,negated_conjecture,
p23(X28,X28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_27) ).
cnf(p23_72,negated_conjecture,
( p23(X247,X246)
| ~ p23(X245,X247)
| ~ p23(X245,X246) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p23_72) ).
cnf(c81,plain,
( p23(X251,X250)
| ~ p23(X250,X251) ),
inference(resolution,[status(thm)],[p23_72,p23_27]) ).
cnf(c84,plain,
p23(c77,c79),
inference(resolution,[status(thm)],[c81,p23_36]) ).
cnf(p24_94,negated_conjecture,
( p24(f25(X434,X435),f25(X433,X432))
| ~ p22(X434,X433)
| ~ p23(X435,X432) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p24_94) ).
cnf(c173,plain,
( p24(f25(X457,c77),f25(X456,c79))
| ~ p22(X457,X456) ),
inference(resolution,[status(thm)],[p24_94,c84]) ).
cnf(c182,plain,
p24(f25(X462,c77),f25(X462,c79)),
inference(resolution,[status(thm)],[c173,p22_28]) ).
cnf(c185,plain,
p24(f25(X463,c79),f25(X463,c77)),
inference(resolution,[status(thm)],[c182,c77]) ).
cnf(p60_42,negated_conjecture,
p60(f25(c75,c79),f21(c76,c78)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p60_42) ).
cnf(p20_29,negated_conjecture,
p20(X30,X30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p20_29) ).
cnf(p60_84,negated_conjecture,
( p60(X336,X337)
| ~ p24(X335,X336)
| ~ p60(X335,X338)
| ~ p20(X338,X337) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p60_84) ).
cnf(c130,plain,
( p60(X346,X348)
| ~ p24(X347,X346)
| ~ p60(X347,X348) ),
inference(resolution,[status(thm)],[p60_84,p20_29]) ).
cnf(c137,plain,
( p60(X590,f21(c76,c78))
| ~ p24(f25(c75,c79),X590) ),
inference(resolution,[status(thm)],[c130,p60_42]) ).
cnf(c236,plain,
p60(f25(c75,c77),f21(c76,c78)),
inference(resolution,[status(thm)],[c137,c185]) ).
cnf(p59_44,negated_conjecture,
p59(f29(c73,f31(f33(c74,c77),c78)),c72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p59_44) ).
cnf(not_p60_107,negated_conjecture,
( ~ p60(f25(c75,X585),f21(c76,X586))
| ~ p59(f29(c73,f31(f33(c74,X584),X586)),c72)
| ~ p59(f29(c73,f31(f33(c74,X585),X583)),c72) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p60_107) ).
cnf(c230,plain,
( ~ p60(f25(c75,X733),f21(c76,X734))
| ~ p59(f29(c73,f31(f33(c74,X733),X734)),c72) ),
inference(factor,[status(thm)],[not_p60_107]) ).
cnf(c364,plain,
~ p60(f25(c75,c77),f21(c76,c78)),
inference(resolution,[status(thm)],[c230,p59_44]) ).
cnf(c365,plain,
$false,
inference(resolution,[status(thm)],[c364,c236]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN717-1 : TPTP v8.1.2. Released v2.5.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.36 % Computer : n020.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Wed May 8 20:31:23 EDT 2024
% 0.16/0.36 % CPUTime :
% 0.70/0.89 % Version: 1.5
% 0.70/0.89 % SZS status Unsatisfiable
% 0.70/0.89 % SZS output start CNFRefutation
% See solution above
% 0.70/0.90
% 0.70/0.90 % Initial clauses : 113
% 0.70/0.90 % Processed clauses : 245
% 0.70/0.90 % Factors computed : 36
% 0.70/0.90 % Resolvents computed: 330
% 0.70/0.90 % Tautologies deleted: 0
% 0.70/0.90 % Forward subsumed : 164
% 0.70/0.90 % Backward subsumed : 0
% 0.70/0.90 % -------- CPU Time ---------
% 0.70/0.90 % User time : 0.504 s
% 0.70/0.90 % System time : 0.023 s
% 0.70/0.90 % Total time : 0.527 s
%------------------------------------------------------------------------------