%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET642+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:39:54 EDT 2024
% Result : Theorem 191.25s 191.53s
% Output : Refutation 191.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET642+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 18:49:22 EDT 2024
% 0.14/0.34 % CPUTime :
% 191.25/191.53 % Version: 1.5
% 191.25/191.53 % SZS status Theorem
% 191.25/191.53 % SZS output start CNFRefutation
% 191.25/191.53 fof(prove_relset_1_4,conjecture,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,set_type)=>(![E]:(ilf_type(E,relation_type(C,D))=>(subset(B,E)=>ilf_type(B,relation_type(C,D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_relset_1_4)).
% 191.25/191.53 fof(c11,negated_conjecture,(~(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,set_type)=>(![E]:(ilf_type(E,relation_type(C,D))=>(subset(B,E)=>ilf_type(B,relation_type(C,D)))))))))))),inference(assume_negation,[status(cth)],[prove_relset_1_4])).
% 191.25/191.53 fof(c12,negated_conjecture,(?[B]:(ilf_type(B,set_type)&(?[C]:(ilf_type(C,set_type)&(?[D]:(ilf_type(D,set_type)&(?[E]:(ilf_type(E,relation_type(C,D))&(subset(B,E)&~ilf_type(B,relation_type(C,D))))))))))),inference(fof_nnf,[status(thm)],[c11])).
% 191.25/191.53 fof(c13,negated_conjecture,(?[X2]:(ilf_type(X2,set_type)&(?[X3]:(ilf_type(X3,set_type)&(?[X4]:(ilf_type(X4,set_type)&(?[X5]:(ilf_type(X5,relation_type(X3,X4))&(subset(X2,X5)&~ilf_type(X2,relation_type(X3,X4))))))))))),inference(variable_rename,[status(thm)],[c12])).
% 191.25/191.53 fof(c14,negated_conjecture,(ilf_type(skolem0001,set_type)&(ilf_type(skolem0002,set_type)&(ilf_type(skolem0003,set_type)&(ilf_type(skolem0004,relation_type(skolem0002,skolem0003))&(subset(skolem0001,skolem0004)&~ilf_type(skolem0001,relation_type(skolem0002,skolem0003))))))),inference(skolemize,[status(esa)],[c13])).
% 191.25/191.53 cnf(c20,negated_conjecture,~ilf_type(skolem0001,relation_type(skolem0002,skolem0003)),inference(split_conjunct,[status(thm)],[c14])).
% 191.25/191.53 fof(p19,axiom,(![B]:ilf_type(B,set_type)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p19)).
% 191.25/191.53 fof(c21,plain,(![X6]:ilf_type(X6,set_type)),inference(variable_rename,[status(thm)],[p19])).
% 191.25/191.53 cnf(c22,plain,ilf_type(X58,set_type),inference(split_conjunct,[status(thm)],[c21])).
% 191.25/191.53 fof(p2,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,set_type)=>(subset(B,cross_product(C,D))=>ilf_type(B,relation_type(C,D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p2)).
% 191.25/191.53 fof(c118,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|(![D]:(~ilf_type(D,set_type)|(~subset(B,cross_product(C,D))|ilf_type(B,relation_type(C,D))))))))),inference(fof_nnf,[status(thm)],[p2])).
% 191.25/191.53 fof(c120,plain,(![X50]:(![X51]:(![X52]:(~ilf_type(X50,set_type)|(~ilf_type(X51,set_type)|(~ilf_type(X52,set_type)|(~subset(X50,cross_product(X51,X52))|ilf_type(X50,relation_type(X51,X52))))))))),inference(shift_quantors,[status(thm)],[fof(c119,plain,(![X50]:(~ilf_type(X50,set_type)|(![X51]:(~ilf_type(X51,set_type)|(![X52]:(~ilf_type(X52,set_type)|(~subset(X50,cross_product(X51,X52))|ilf_type(X50,relation_type(X51,X52))))))))),inference(variable_rename,[status(thm)],[c118])).])).
% 191.25/191.53 cnf(c121,plain,~ilf_type(X368,set_type)|~ilf_type(X370,set_type)|~ilf_type(X369,set_type)|~subset(X368,cross_product(X370,X369))|ilf_type(X368,relation_type(X370,X369)),inference(split_conjunct,[status(thm)],[c120])).
% 191.25/191.53 cnf(c19,negated_conjecture,subset(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c14])).
% 191.25/191.53 cnf(c18,negated_conjecture,ilf_type(skolem0004,relation_type(skolem0002,skolem0003)),inference(split_conjunct,[status(thm)],[c14])).
% 191.25/191.53 fof(p1,axiom,(![B]:(ilf_type(B,set_type)=>(![C]:(ilf_type(C,set_type)=>(![D]:(ilf_type(D,set_type)=>(![E]:(ilf_type(E,relation_type(C,D))=>(subset(B,E)=>subset(B,cross_product(C,D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p1)).
% 191.25/191.53 fof(c122,plain,(![B]:(~ilf_type(B,set_type)|(![C]:(~ilf_type(C,set_type)|(![D]:(~ilf_type(D,set_type)|(![E]:(~ilf_type(E,relation_type(C,D))|(~subset(B,E)|subset(B,cross_product(C,D))))))))))),inference(fof_nnf,[status(thm)],[p1])).
% 191.25/191.53 fof(c124,plain,(![X53]:(![X54]:(![X55]:(![X56]:(~ilf_type(X53,set_type)|(~ilf_type(X54,set_type)|(~ilf_type(X55,set_type)|(~ilf_type(X56,relation_type(X54,X55))|(~subset(X53,X56)|subset(X53,cross_product(X54,X55))))))))))),inference(shift_quantors,[status(thm)],[fof(c123,plain,(![X53]:(~ilf_type(X53,set_type)|(![X54]:(~ilf_type(X54,set_type)|(![X55]:(~ilf_type(X55,set_type)|(![X56]:(~ilf_type(X56,relation_type(X54,X55))|(~subset(X53,X56)|subset(X53,cross_product(X54,X55))))))))))),inference(variable_rename,[status(thm)],[c122])).])).
% 191.25/191.53 cnf(c125,plain,~ilf_type(X384,set_type)|~ilf_type(X387,set_type)|~ilf_type(X386,set_type)|~ilf_type(X385,relation_type(X387,X386))|~subset(X384,X385)|subset(X384,cross_product(X387,X386)),inference(split_conjunct,[status(thm)],[c124])).
% 191.25/191.53 cnf(c321,plain,~ilf_type(X1065,set_type)|~ilf_type(skolem0002,set_type)|~ilf_type(skolem0003,set_type)|~subset(X1065,skolem0004)|subset(X1065,cross_product(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c125, c18])).
% 191.25/191.53 cnf(c953,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|~ilf_type(skolem0003,set_type)|subset(skolem0001,cross_product(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c321, c19])).
% 191.25/191.53 cnf(c12257,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|subset(skolem0001,cross_product(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c953, c22])).
% 191.25/191.53 cnf(c12275,plain,~ilf_type(skolem0001,set_type)|subset(skolem0001,cross_product(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c12257, c22])).
% 191.25/191.53 cnf(c12276,plain,subset(skolem0001,cross_product(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c12275, c22])).
% 191.25/191.53 cnf(c12280,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|~ilf_type(skolem0003,set_type)|ilf_type(skolem0001,relation_type(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c12276, c121])).
% 191.25/191.53 cnf(c130122,plain,~ilf_type(skolem0001,set_type)|~ilf_type(skolem0002,set_type)|ilf_type(skolem0001,relation_type(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c12280, c22])).
% 191.25/191.53 cnf(c130123,plain,~ilf_type(skolem0001,set_type)|ilf_type(skolem0001,relation_type(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c130122, c22])).
% 191.25/191.53 cnf(c130124,plain,ilf_type(skolem0001,relation_type(skolem0002,skolem0003)),inference(resolution,[status(thm)],[c130123, c22])).
% 191.25/191.53 cnf(c132215,plain,$false,inference(resolution,[status(thm)],[c130124, c20])).
% 191.25/191.53 % SZS output end CNFRefutation
% 191.25/191.53
% 191.25/191.53 % Initial clauses : 56
% 191.25/191.53 % Processed clauses : 4331
% 191.25/191.53 % Factors computed : 761
% 191.25/191.53 % Resolvents computed: 131330
% 191.25/191.53 % Tautologies deleted: 28
% 191.25/191.53 % Forward subsumed : 3976
% 191.25/191.53 % Backward subsumed : 1248
% 191.25/191.53 % -------- CPU Time ---------
% 191.25/191.53 % User time : 190.606 s
% 191.25/191.53 % System time : 0.518 s
% 191.25/191.53 % Total time : 191.124 s
%------------------------------------------------------------------------------