%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP204-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %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 : Thu May 9 17:34:36 EDT 2024
% Result : Unsatisfiable 0.81s 0.99s
% Output : Refutation 0.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of clauses : 27 ( 15 unt; 0 nHn; 26 RR)
% Number of literals : 42 ( 11 equ; 17 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 28 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause87,negated_conjecture,
man(skc12,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(clause34,axiom,
( ~ man(X70,X69)
| male(X70,X69) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c118,plain,
male(skc12,skc16),
inference(resolution,[status(thm)],[clause34,clause87]) ).
cnf(clause60,axiom,
( ~ male(X122,X121)
| ~ unisex(X122,X121) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(symmetry,axiom,
( X141 != X142
| X142 = X141 ),
theory(equality) ).
cnf(clause67,axiom,
( ~ be(X138,X135,X137,X136)
| X137 = X136 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(clause106,negated_conjecture,
be(skc12,skc14,skc16,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
cnf(c218,plain,
skc16 = skc13,
inference(resolution,[status(thm)],[clause106,clause67]) ).
cnf(c220,plain,
skc13 = skc16,
inference(resolution,[status(thm)],[c218,symmetry]) ).
cnf(clause91,negated_conjecture,
wheel(skc12,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
cnf(clause10,axiom,
( ~ wheel(X22,X21)
| device(X22,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c90,plain,
device(skc12,skc13),
inference(resolution,[status(thm)],[clause10,clause91]) ).
cnf(clause11,axiom,
( ~ device(X24,X23)
| instrumentality(X24,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c92,plain,
instrumentality(skc12,skc13),
inference(resolution,[status(thm)],[clause11,c90]) ).
cnf(clause12,axiom,
( ~ instrumentality(X26,X25)
| artifact(X26,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c93,plain,
artifact(skc12,skc13),
inference(resolution,[status(thm)],[clause12,c92]) ).
cnf(clause13,axiom,
( ~ artifact(X28,X27)
| object(X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c94,plain,
object(skc12,skc13),
inference(resolution,[status(thm)],[clause13,c93]) ).
cnf(clause20,axiom,
( ~ object(X42,X41)
| unisex(X42,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c102,plain,
unisex(skc12,skc13),
inference(resolution,[status(thm)],[clause20,c94]) ).
cnf(c13,axiom,
( X332 != X333
| X330 != X331
| ~ unisex(X332,X330)
| unisex(X333,X331) ),
theory(equality) ).
cnf(c670,plain,
( skc12 != X548
| skc13 != X547
| unisex(X548,X547) ),
inference(resolution,[status(thm)],[c13,c102]) ).
cnf(c909,plain,
( skc12 != X549
| unisex(X549,skc16) ),
inference(resolution,[status(thm)],[c670,c220]) ).
cnf(c911,plain,
unisex(skc12,skc16),
inference(resolution,[status(thm)],[c909,reflexivity]) ).
cnf(c914,plain,
~ male(skc12,skc16),
inference(resolution,[status(thm)],[c911,clause60]) ).
cnf(c915,plain,
$false,
inference(resolution,[status(thm)],[c914,c118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP204-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 13:26:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.81/0.99 % Version: 1.5
% 0.81/0.99 % SZS status Unsatisfiable
% 0.81/0.99 % SZS output start CNFRefutation
% See solution above
% 0.81/0.99
% 0.81/0.99 % Initial clauses : 200
% 0.81/0.99 % Processed clauses : 475
% 0.81/0.99 % Factors computed : 10
% 0.81/0.99 % Resolvents computed: 829
% 0.81/0.99 % Tautologies deleted: 3
% 0.81/0.99 % Forward subsumed : 88
% 0.81/0.99 % Backward subsumed : 2
% 0.81/0.99 % -------- CPU Time ---------
% 0.81/0.99 % User time : 0.634 s
% 0.81/0.99 % System time : 0.015 s
% 0.81/0.99 % Total time : 0.649 s
%------------------------------------------------------------------------------