%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU177+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:40:46 EDT 2024
% Result : Theorem 1.32s 1.48s
% Output : Refutation 1.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU177+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n005.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 11:10:53 EDT 2024
% 0.15/0.36 % CPUTime :
% 1.32/1.48 % Version: 1.5
% 1.32/1.48 % SZS status Theorem
% 1.32/1.48 % SZS output start CNFRefutation
% 1.32/1.48 fof(t20_relat_1,conjecture,(![A]:(![B]:(![C]:(relation(C)=>(in(ordered_pair(A,B),C)=>(in(A,relation_dom(C))&in(B,relation_rng(C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t20_relat_1)).
% 1.32/1.48 fof(c29,negated_conjecture,(~(![A]:(![B]:(![C]:(relation(C)=>(in(ordered_pair(A,B),C)=>(in(A,relation_dom(C))&in(B,relation_rng(C))))))))),inference(assume_negation,[status(cth)],[t20_relat_1])).
% 1.32/1.48 fof(c30,negated_conjecture,(?[A]:(?[B]:(?[C]:(relation(C)&(in(ordered_pair(A,B),C)&(~in(A,relation_dom(C))|~in(B,relation_rng(C)))))))),inference(fof_nnf,[status(thm)],[c29])).
% 1.32/1.48 fof(c31,negated_conjecture,(?[X22]:(?[X23]:(?[X24]:(relation(X24)&(in(ordered_pair(X22,X23),X24)&(~in(X22,relation_dom(X24))|~in(X23,relation_rng(X24)))))))),inference(variable_rename,[status(thm)],[c30])).
% 1.32/1.48 fof(c32,negated_conjecture,(relation(skolem0009)&(in(ordered_pair(skolem0007,skolem0008),skolem0009)&(~in(skolem0007,relation_dom(skolem0009))|~in(skolem0008,relation_rng(skolem0009))))),inference(skolemize,[status(esa)],[c31])).
% 1.32/1.48 cnf(c35,negated_conjecture,~in(skolem0007,relation_dom(skolem0009))|~in(skolem0008,relation_rng(skolem0009)),inference(split_conjunct,[status(thm)],[c32])).
% 1.32/1.48 cnf(c33,negated_conjecture,relation(skolem0009),inference(split_conjunct,[status(thm)],[c32])).
% 1.32/1.48 cnf(reflexivity,axiom,X50=X50,theory(equality)).
% 1.32/1.48 cnf(c34,negated_conjecture,in(ordered_pair(skolem0007,skolem0008),skolem0009),inference(split_conjunct,[status(thm)],[c32])).
% 1.32/1.48 fof(d5_relat_1,axiom,(![A]:(relation(A)=>(![B]:(B=relation_rng(A)<=>(![C]:(in(C,B)<=>(?[D]:in(ordered_pair(D,C),A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d5_relat_1)).
% 1.32/1.48 fof(c9,plain,(![A]:(~relation(A)|(![B]:((B!=relation_rng(A)|(![C]:((~in(C,B)|(?[D]:in(ordered_pair(D,C),A)))&((![D]:~in(ordered_pair(D,C),A))|in(C,B)))))&((?[C]:((~in(C,B)|(![D]:~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]:in(ordered_pair(D,C),A)))))|B=relation_rng(A)))))),inference(fof_nnf,[status(thm)],[d5_relat_1])).
% 1.32/1.48 fof(c10,plain,(![A]:(~relation(A)|((![B]:(B!=relation_rng(A)|((![C]:(~in(C,B)|(?[D]:in(ordered_pair(D,C),A))))&(![C]:((![D]:~in(ordered_pair(D,C),A))|in(C,B))))))&(![B]:((?[C]:((~in(C,B)|(![D]:~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]:in(ordered_pair(D,C),A)))))|B=relation_rng(A)))))),inference(shift_quantors,[status(thm)],[c9])).
% 1.32/1.48 fof(c11,plain,(![X2]:(~relation(X2)|((![X3]:(X3!=relation_rng(X2)|((![X4]:(~in(X4,X3)|(?[X5]:in(ordered_pair(X5,X4),X2))))&(![X6]:((![X7]:~in(ordered_pair(X7,X6),X2))|in(X6,X3))))))&(![X8]:((?[X9]:((~in(X9,X8)|(![X10]:~in(ordered_pair(X10,X9),X2)))&(in(X9,X8)|(?[X11]:in(ordered_pair(X11,X9),X2)))))|X8=relation_rng(X2)))))),inference(variable_rename,[status(thm)],[c10])).
% 1.32/1.48 fof(c13,plain,(![X2]:(![X3]:(![X4]:(![X6]:(![X7]:(![X8]:(![X10]:(~relation(X2)|((X3!=relation_rng(X2)|((~in(X4,X3)|in(ordered_pair(skolem0001(X2,X3,X4),X4),X2))&(~in(ordered_pair(X7,X6),X2)|in(X6,X3))))&(((~in(skolem0002(X2,X8),X8)|~in(ordered_pair(X10,skolem0002(X2,X8)),X2))&(in(skolem0002(X2,X8),X8)|in(ordered_pair(skolem0003(X2,X8),skolem0002(X2,X8)),X2)))|X8=relation_rng(X2))))))))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,(![X2]:(~relation(X2)|((![X3]:(X3!=relation_rng(X2)|((![X4]:(~in(X4,X3)|in(ordered_pair(skolem0001(X2,X3,X4),X4),X2)))&(![X6]:((![X7]:~in(ordered_pair(X7,X6),X2))|in(X6,X3))))))&(![X8]:(((~in(skolem0002(X2,X8),X8)|(![X10]:~in(ordered_pair(X10,skolem0002(X2,X8)),X2)))&(in(skolem0002(X2,X8),X8)|in(ordered_pair(skolem0003(X2,X8),skolem0002(X2,X8)),X2)))|X8=relation_rng(X2)))))),inference(skolemize,[status(esa)],[c11])).])).
% 1.32/1.48 fof(c14,plain,(![X2]:(![X3]:(![X4]:(![X6]:(![X7]:(![X8]:(![X10]:(((~relation(X2)|(X3!=relation_rng(X2)|(~in(X4,X3)|in(ordered_pair(skolem0001(X2,X3,X4),X4),X2))))&(~relation(X2)|(X3!=relation_rng(X2)|(~in(ordered_pair(X7,X6),X2)|in(X6,X3)))))&((~relation(X2)|((~in(skolem0002(X2,X8),X8)|~in(ordered_pair(X10,skolem0002(X2,X8)),X2))|X8=relation_rng(X2)))&(~relation(X2)|((in(skolem0002(X2,X8),X8)|in(ordered_pair(skolem0003(X2,X8),skolem0002(X2,X8)),X2))|X8=relation_rng(X2)))))))))))),inference(distribute,[status(thm)],[c13])).
% 1.32/1.48 cnf(c16,plain,~relation(X115)|X113!=relation_rng(X115)|~in(ordered_pair(X116,X114),X115)|in(X114,X113),inference(split_conjunct,[status(thm)],[c14])).
% 1.32/1.48 cnf(c175,plain,~relation(skolem0009)|X243!=relation_rng(skolem0009)|in(skolem0008,X243),inference(resolution,[status(thm)],[c16, c34])).
% 1.32/1.48 cnf(c1137,plain,~relation(skolem0009)|in(skolem0008,relation_rng(skolem0009)),inference(resolution,[status(thm)],[c175, reflexivity])).
% 1.32/1.48 cnf(c2507,plain,in(skolem0008,relation_rng(skolem0009)),inference(resolution,[status(thm)],[c1137, c33])).
% 1.32/1.48 cnf(c2579,plain,~in(skolem0007,relation_dom(skolem0009)),inference(resolution,[status(thm)],[c2507, c35])).
% 1.32/1.48 fof(d4_relat_1,axiom,(![A]:(relation(A)=>(![B]:(B=relation_dom(A)<=>(![C]:(in(C,B)<=>(?[D]:in(ordered_pair(C,D),A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_relat_1)).
% 1.32/1.48 fof(c19,plain,(![A]:(~relation(A)|(![B]:((B!=relation_dom(A)|(![C]:((~in(C,B)|(?[D]:in(ordered_pair(C,D),A)))&((![D]:~in(ordered_pair(C,D),A))|in(C,B)))))&((?[C]:((~in(C,B)|(![D]:~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]:in(ordered_pair(C,D),A)))))|B=relation_dom(A)))))),inference(fof_nnf,[status(thm)],[d4_relat_1])).
% 1.32/1.48 fof(c20,plain,(![A]:(~relation(A)|((![B]:(B!=relation_dom(A)|((![C]:(~in(C,B)|(?[D]:in(ordered_pair(C,D),A))))&(![C]:((![D]:~in(ordered_pair(C,D),A))|in(C,B))))))&(![B]:((?[C]:((~in(C,B)|(![D]:~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]:in(ordered_pair(C,D),A)))))|B=relation_dom(A)))))),inference(shift_quantors,[status(thm)],[c19])).
% 1.32/1.48 fof(c21,plain,(![X12]:(~relation(X12)|((![X13]:(X13!=relation_dom(X12)|((![X14]:(~in(X14,X13)|(?[X15]:in(ordered_pair(X14,X15),X12))))&(![X16]:((![X17]:~in(ordered_pair(X16,X17),X12))|in(X16,X13))))))&(![X18]:((?[X19]:((~in(X19,X18)|(![X20]:~in(ordered_pair(X19,X20),X12)))&(in(X19,X18)|(?[X21]:in(ordered_pair(X19,X21),X12)))))|X18=relation_dom(X12)))))),inference(variable_rename,[status(thm)],[c20])).
% 1.32/1.48 fof(c23,plain,(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:(![X20]:(~relation(X12)|((X13!=relation_dom(X12)|((~in(X14,X13)|in(ordered_pair(X14,skolem0004(X12,X13,X14)),X12))&(~in(ordered_pair(X16,X17),X12)|in(X16,X13))))&(((~in(skolem0005(X12,X18),X18)|~in(ordered_pair(skolem0005(X12,X18),X20),X12))&(in(skolem0005(X12,X18),X18)|in(ordered_pair(skolem0005(X12,X18),skolem0006(X12,X18)),X12)))|X18=relation_dom(X12))))))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,(![X12]:(~relation(X12)|((![X13]:(X13!=relation_dom(X12)|((![X14]:(~in(X14,X13)|in(ordered_pair(X14,skolem0004(X12,X13,X14)),X12)))&(![X16]:((![X17]:~in(ordered_pair(X16,X17),X12))|in(X16,X13))))))&(![X18]:(((~in(skolem0005(X12,X18),X18)|(![X20]:~in(ordered_pair(skolem0005(X12,X18),X20),X12)))&(in(skolem0005(X12,X18),X18)|in(ordered_pair(skolem0005(X12,X18),skolem0006(X12,X18)),X12)))|X18=relation_dom(X12)))))),inference(skolemize,[status(esa)],[c21])).])).
% 1.32/1.48 fof(c24,plain,(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:(![X20]:(((~relation(X12)|(X13!=relation_dom(X12)|(~in(X14,X13)|in(ordered_pair(X14,skolem0004(X12,X13,X14)),X12))))&(~relation(X12)|(X13!=relation_dom(X12)|(~in(ordered_pair(X16,X17),X12)|in(X16,X13)))))&((~relation(X12)|((~in(skolem0005(X12,X18),X18)|~in(ordered_pair(skolem0005(X12,X18),X20),X12))|X18=relation_dom(X12)))&(~relation(X12)|((in(skolem0005(X12,X18),X18)|in(ordered_pair(skolem0005(X12,X18),skolem0006(X12,X18)),X12))|X18=relation_dom(X12)))))))))))),inference(distribute,[status(thm)],[c23])).
% 1.32/1.48 cnf(c26,plain,~relation(X130)|X133!=relation_dom(X130)|~in(ordered_pair(X131,X132),X130)|in(X131,X133),inference(split_conjunct,[status(thm)],[c24])).
% 1.32/1.48 cnf(c226,plain,~relation(skolem0009)|X368!=relation_dom(skolem0009)|in(skolem0007,X368),inference(resolution,[status(thm)],[c26, c34])).
% 1.32/1.48 cnf(c3373,plain,~relation(skolem0009)|in(skolem0007,relation_dom(skolem0009)),inference(resolution,[status(thm)],[c226, reflexivity])).
% 1.32/1.48 cnf(c3627,plain,in(skolem0007,relation_dom(skolem0009)),inference(resolution,[status(thm)],[c3373, c33])).
% 1.32/1.48 cnf(c3665,plain,$false,inference(resolution,[status(thm)],[c3627, c2579])).
% 1.32/1.48 % SZS output end CNFRefutation
% 1.32/1.48
% 1.32/1.48 % Initial clauses : 47
% 1.32/1.48 % Processed clauses : 267
% 1.32/1.48 % Factors computed : 5
% 1.32/1.48 % Resolvents computed: 3575
% 1.32/1.48 % Tautologies deleted: 5
% 1.32/1.48 % Forward subsumed : 191
% 1.32/1.48 % Backward subsumed : 5
% 1.32/1.48 % -------- CPU Time ---------
% 1.32/1.48 % User time : 1.094 s
% 1.32/1.48 % System time : 0.023 s
% 1.32/1.48 % Total time : 1.117 s
%------------------------------------------------------------------------------