%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV405+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:44:55 EDT 2024
% Result : Theorem 0.59s 0.76s
% Output : Refutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV405+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n010.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.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 05:56:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.59/0.76 % Version: 1.5
% 0.59/0.76 % SZS status Theorem
% 0.59/0.76 % SZS output start CNFRefutation
% 0.59/0.76 fof(ax22,axiom,(![U]:(![V]:(~pair_in_list(create_slb,U,V)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+2.ax', ax22)).
% 0.59/0.76 fof(c150,plain,(![U]:(![V]:~pair_in_list(create_slb,U,V))),inference(fof_simplification,[status(thm)],[ax22])).
% 0.59/0.76 fof(c151,plain,(![X111]:(![X112]:~pair_in_list(create_slb,X111,X112))),inference(variable_rename,[status(thm)],[c150])).
% 0.59/0.76 cnf(c152,plain,~pair_in_list(create_slb,X145,X144),inference(split_conjunct,[status(thm)],[c151])).
% 0.59/0.76 fof(ax36,axiom,(![U]:(![V]:check_cpq(triple(U,create_slb,V)))),file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+3.ax', ax36)).
% 0.59/0.76 fof(c99,plain,(![X65]:(![X66]:check_cpq(triple(X65,create_slb,X66)))),inference(variable_rename,[status(thm)],[ax36])).
% 0.59/0.76 cnf(c100,plain,check_cpq(triple(X153,create_slb,X152)),inference(split_conjunct,[status(thm)],[c99])).
% 0.59/0.76 fof(l41_co,conjecture,(![U]:(![V]:(check_cpq(triple(U,create_slb,V))<=>(![W]:(![X]:(pair_in_list(create_slb,W,X)=>less_than(X,W))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l41_co)).
% 0.59/0.76 fof(c24,negated_conjecture,(~(![U]:(![V]:(check_cpq(triple(U,create_slb,V))<=>(![W]:(![X]:(pair_in_list(create_slb,W,X)=>less_than(X,W)))))))),inference(assume_negation,[status(cth)],[l41_co])).
% 0.59/0.76 fof(c25,negated_conjecture,(?[U]:(?[V]:((~check_cpq(triple(U,create_slb,V))|(?[W]:(?[X]:(pair_in_list(create_slb,W,X)&~less_than(X,W)))))&(check_cpq(triple(U,create_slb,V))|(![W]:(![X]:(~pair_in_list(create_slb,W,X)|less_than(X,W)))))))),inference(fof_nnf,[status(thm)],[c24])).
% 0.59/0.76 fof(c26,negated_conjecture,(?[X2]:(?[X3]:((~check_cpq(triple(X2,create_slb,X3))|(?[X4]:(?[X5]:(pair_in_list(create_slb,X4,X5)&~less_than(X5,X4)))))&(check_cpq(triple(X2,create_slb,X3))|(![X6]:(![X7]:(~pair_in_list(create_slb,X6,X7)|less_than(X7,X6)))))))),inference(variable_rename,[status(thm)],[c25])).
% 0.59/0.76 fof(c28,negated_conjecture,(![X6]:(![X7]:((~check_cpq(triple(skolem0001,create_slb,skolem0002))|(pair_in_list(create_slb,skolem0003,skolem0004)&~less_than(skolem0004,skolem0003)))&(check_cpq(triple(skolem0001,create_slb,skolem0002))|(~pair_in_list(create_slb,X6,X7)|less_than(X7,X6)))))),inference(shift_quantors,[status(thm)],[fof(c27,negated_conjecture,((~check_cpq(triple(skolem0001,create_slb,skolem0002))|(pair_in_list(create_slb,skolem0003,skolem0004)&~less_than(skolem0004,skolem0003)))&(check_cpq(triple(skolem0001,create_slb,skolem0002))|(![X6]:(![X7]:(~pair_in_list(create_slb,X6,X7)|less_than(X7,X6)))))),inference(skolemize,[status(esa)],[c26])).])).
% 0.59/0.76 fof(c29,negated_conjecture,(![X6]:(![X7]:(((~check_cpq(triple(skolem0001,create_slb,skolem0002))|pair_in_list(create_slb,skolem0003,skolem0004))&(~check_cpq(triple(skolem0001,create_slb,skolem0002))|~less_than(skolem0004,skolem0003)))&(check_cpq(triple(skolem0001,create_slb,skolem0002))|(~pair_in_list(create_slb,X6,X7)|less_than(X7,X6)))))),inference(distribute,[status(thm)],[c28])).
% 0.59/0.76 cnf(c30,negated_conjecture,~check_cpq(triple(skolem0001,create_slb,skolem0002))|pair_in_list(create_slb,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c29])).
% 0.59/0.76 cnf(c623,plain,pair_in_list(create_slb,skolem0003,skolem0004),inference(resolution,[status(thm)],[c30, c100])).
% 0.59/0.76 cnf(c624,plain,$false,inference(resolution,[status(thm)],[c623, c152])).
% 0.59/0.76 % SZS output end CNFRefutation
% 0.59/0.76
% 0.59/0.76 % Initial clauses : 80
% 0.59/0.76 % Processed clauses : 120
% 0.59/0.76 % Factors computed : 13
% 0.59/0.76 % Resolvents computed: 427
% 0.59/0.76 % Tautologies deleted: 6
% 0.59/0.76 % Forward subsumed : 19
% 0.59/0.76 % Backward subsumed : 2
% 0.59/0.76 % -------- CPU Time ---------
% 0.59/0.76 % User time : 0.389 s
% 0.59/0.76 % System time : 0.017 s
% 0.59/0.76 % Total time : 0.406 s
%------------------------------------------------------------------------------