↑ Up

PyRes---1.5.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : GEO219+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n028.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:21:35 EDT 2024

% Result   : Theorem 0.77s 0.93s
% Output   : Refutation 0.77s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : GEO219+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35  % Computer : n028.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35  % CPULimit : 300
% 0.14/0.35  % WCLimit  : 300
% 0.14/0.35  % DateTime : Thu May  9 08:17:53 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 0.77/0.93  % Version:  1.5
% 0.77/0.93  % SZS status Theorem
% 0.77/0.93  % SZS output start CNFRefutation
% 0.77/0.93  fof(con,conjecture,(![L]:(![M]:(![N]:((orthogonal_lines(L,M)&parallel_lines(L,N))=>orthogonal_lines(M,N))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.77/0.93  fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:((orthogonal_lines(L,M)&parallel_lines(L,N))=>orthogonal_lines(M,N)))))),inference(assume_negation,[status(cth)],[con])).
% 0.77/0.93  fof(c1,negated_conjecture,(?[L]:(?[M]:(?[N]:((orthogonal_lines(L,M)&parallel_lines(L,N))&~orthogonal_lines(M,N))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.77/0.93  fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((orthogonal_lines(X2,X3)&parallel_lines(X2,X4))&~orthogonal_lines(X3,X4))))),inference(variable_rename,[status(thm)],[c1])).
% 0.77/0.93  fof(c3,negated_conjecture,((orthogonal_lines(skolem0001,skolem0002)&parallel_lines(skolem0001,skolem0003))&~orthogonal_lines(skolem0002,skolem0003)),inference(skolemize,[status(esa)],[c2])).
% 0.77/0.93  cnf(c5,negated_conjecture,parallel_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.93  fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a3)).
% 0.77/0.93  fof(c21,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 0.77/0.93  fof(c22,plain,(![X]:(![Y]:((~parallel_lines(X,Y)|~convergent_lines(X,Y))&(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c21])).
% 0.77/0.93  fof(c23,plain,((![X]:(![Y]:(~parallel_lines(X,Y)|~convergent_lines(X,Y))))&(![X]:(![Y]:(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c22])).
% 0.77/0.93  fof(c25,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~parallel_lines(X13,X14)|~convergent_lines(X13,X14))&(convergent_lines(X15,X16)|parallel_lines(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X13]:(![X14]:(~parallel_lines(X13,X14)|~convergent_lines(X13,X14))))&(![X15]:(![X16]:(convergent_lines(X15,X16)|parallel_lines(X15,X16))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.77/0.93  cnf(c26,plain,~parallel_lines(X117,X118)|~convergent_lines(X117,X118),inference(split_conjunct,[status(thm)],[c25])).
% 0.77/0.93  cnf(c4,negated_conjecture,orthogonal_lines(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.93  fof(a5,axiom,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>(~unorthogonal_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a5)).
% 0.77/0.93  fof(c7,plain,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>~unorthogonal_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5])).
% 0.77/0.93  fof(c8,plain,(![X]:(![Y]:((~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))&(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.77/0.93  fof(c9,plain,((![X]:(![Y]:(~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))))&(![X]:(![Y]:(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c8])).
% 0.77/0.93  fof(c11,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))&(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,((![X5]:(![X6]:(~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))))&(![X7]:(![X8]:(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.77/0.93  cnf(c12,plain,~orthogonal_lines(X107,X108)|~unorthogonal_lines(X107,X108),inference(split_conjunct,[status(thm)],[c11])).
% 0.77/0.93  fof(p1,axiom,(![X]:(![Y]:(distinct_lines(X,Y)=>convergent_lines(X,Y)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 0.77/0.93  fof(c101,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|convergent_lines(X,Y)))),inference(fof_nnf,[status(thm)],[p1])).
% 0.77/0.93  fof(c102,plain,(![X61]:(![X62]:(~distinct_lines(X61,X62)|convergent_lines(X61,X62)))),inference(variable_rename,[status(thm)],[c101])).
% 0.77/0.93  cnf(c103,plain,~distinct_lines(X164,X163)|convergent_lines(X164,X163),inference(split_conjunct,[status(thm)],[c102])).
% 0.77/0.93  fof(coipo1,axiom,(![L]:(![M]:(~((~convergent_lines(L,M))&(~unorthogonal_lines(L,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', coipo1)).
% 0.77/0.93  fof(c66,plain,(![L]:(![M]:(~(~convergent_lines(L,M)&~unorthogonal_lines(L,M))))),inference(fof_simplification,[status(thm)],[coipo1])).
% 0.77/0.93  fof(c67,plain,(![L]:(![M]:(convergent_lines(L,M)|unorthogonal_lines(L,M)))),inference(fof_nnf,[status(thm)],[c66])).
% 0.77/0.93  fof(c68,plain,(![X39]:(![X40]:(convergent_lines(X39,X40)|unorthogonal_lines(X39,X40)))),inference(variable_rename,[status(thm)],[c67])).
% 0.77/0.93  cnf(c69,plain,convergent_lines(X141,X140)|unorthogonal_lines(X141,X140),inference(split_conjunct,[status(thm)],[c68])).
% 0.77/0.93  cnf(c180,plain,convergent_lines(X185,X186)|~orthogonal_lines(X185,X186),inference(resolution,[status(thm)],[c69, c12])).
% 0.77/0.93  cnf(c202,plain,convergent_lines(skolem0001,skolem0002),inference(resolution,[status(thm)],[c180, c4])).
% 0.77/0.93  fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 0.77/0.93  fof(c104,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 0.77/0.93  fof(c105,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c104])).
% 0.77/0.93  fof(c107,plain,(![X63]:(![X64]:(![X65]:(~convergent_lines(X63,X64)|(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X63]:(![X64]:(~convergent_lines(X63,X64)|(![X65]:(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(variable_rename,[status(thm)],[c105])).])).
% 0.77/0.93  cnf(c108,plain,~convergent_lines(X301,X302)|distinct_lines(X302,X300)|convergent_lines(X301,X300),inference(split_conjunct,[status(thm)],[c107])).
% 0.77/0.93  cnf(c359,plain,distinct_lines(skolem0002,X303)|convergent_lines(skolem0001,X303),inference(resolution,[status(thm)],[c108, c202])).
% 0.77/0.93  cnf(c366,plain,distinct_lines(skolem0002,X312)|~parallel_lines(skolem0001,X312),inference(resolution,[status(thm)],[c359, c26])).
% 0.77/0.93  cnf(c402,plain,distinct_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c366, c5])).
% 0.77/0.93  cnf(c409,plain,convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c402, c103])).
% 0.77/0.93  cnf(c6,negated_conjecture,~orthogonal_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 0.77/0.93  cnf(c13,plain,unorthogonal_lines(X110,X109)|orthogonal_lines(X110,X109),inference(split_conjunct,[status(thm)],[c11])).
% 0.77/0.93  cnf(c164,plain,unorthogonal_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c13, c6])).
% 0.77/0.93  fof(cotno1,axiom,(![L]:(![M]:(![N]:((((~convergent_lines(L,M))|(~unorthogonal_lines(L,M)))&((~convergent_lines(L,N))|(~unorthogonal_lines(L,N))))=>((~convergent_lines(M,N))|(~unorthogonal_lines(M,N))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 0.77/0.93  fof(c58,plain,(![L]:(![M]:(![N]:(((~convergent_lines(L,M)|~unorthogonal_lines(L,M))&(~convergent_lines(L,N)|~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_simplification,[status(thm)],[cotno1])).
% 0.77/0.93  fof(c59,plain,(![L]:(![M]:(![N]:(((convergent_lines(L,M)&unorthogonal_lines(L,M))|(convergent_lines(L,N)&unorthogonal_lines(L,N)))|(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c58])).
% 0.77/0.93  fof(c60,plain,(![X36]:(![X37]:(![X38]:(((convergent_lines(X36,X37)&unorthogonal_lines(X36,X37))|(convergent_lines(X36,X38)&unorthogonal_lines(X36,X38)))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))),inference(variable_rename,[status(thm)],[c59])).
% 0.77/0.93  fof(c61,plain,(![X36]:(![X37]:(![X38]:((((convergent_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((convergent_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38))))&(((unorthogonal_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((unorthogonal_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))))),inference(distribute,[status(thm)],[c60])).
% 0.77/0.93  cnf(c64,plain,unorthogonal_lines(X208,X210)|convergent_lines(X208,X209)|~convergent_lines(X210,X209)|~unorthogonal_lines(X210,X209),inference(split_conjunct,[status(thm)],[c61])).
% 0.77/0.93  cnf(c231,plain,unorthogonal_lines(X450,skolem0002)|convergent_lines(X450,skolem0003)|~convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c64, c164])).
% 0.77/0.93  cnf(c819,plain,unorthogonal_lines(X494,skolem0002)|convergent_lines(X494,skolem0003),inference(resolution,[status(thm)],[c231, c409])).
% 0.77/0.93  cnf(c940,plain,convergent_lines(X513,skolem0003)|~orthogonal_lines(X513,skolem0002),inference(resolution,[status(thm)],[c819, c12])).
% 0.77/0.93  cnf(c1047,plain,convergent_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c940, c4])).
% 0.77/0.93  cnf(c1060,plain,~parallel_lines(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1047, c26])).
% 0.77/0.93  cnf(c1069,plain,$false,inference(resolution,[status(thm)],[c1060, c5])).
% 0.77/0.93  % SZS output end CNFRefutation
% 0.77/0.93  
% 0.77/0.93  % Initial clauses    : 49
% 0.77/0.93  % Processed clauses  : 190
% 0.77/0.93  % Factors computed   : 9
% 0.77/0.93  % Resolvents computed: 899
% 0.77/0.93  % Tautologies deleted: 8
% 0.77/0.93  % Forward subsumed   : 158
% 0.77/0.93  % Backward subsumed  : 4
% 0.77/0.93  % -------- CPU Time ---------
% 0.77/0.93  % User time          : 0.557 s
% 0.77/0.93  % System time        : 0.023 s
% 0.77/0.93  % Total time         : 0.580 s
%------------------------------------------------------------------------------