%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PLA029+2 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:37:23 EDT 2024
% Result : Satisfiable 0.53s 0.70s
% Output : Saturation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : PLA029+2 : TPTP v8.1.2. Released v2.5.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n018.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 : Wed May 8 21:53:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.53/0.70 % Version: 1.5
% 0.53/0.70 % SZS status Satisfiable
% 0.53/0.70 % SZS output start Saturation
% 0.53/0.70 fof(non_object_remains_on,axiom,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&(~object(V,I)))&on(V,W,I))=>on(V,W,s(I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', non_object_remains_on)).
% 0.53/0.70 fof(c60,plain,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&~object(V,I))&on(V,W,I))=>on(V,W,s(I)))))))),inference(fof_simplification,[status(thm)],[non_object_remains_on])).
% 0.53/0.70 fof(c61,plain,(![I]:(![V]:(~nonfixed(V)|(![W]:((~a_block(W)|~neq(V,W))|(((~time(I)|object(V,I))|~on(V,W,I))|on(V,W,s(I)))))))),inference(fof_nnf,[status(thm)],[c60])).
% 0.53/0.70 fof(c63,plain,(![X44]:(![X45]:(![X46]:(~nonfixed(X45)|((~a_block(X46)|~neq(X45,X46))|(((~time(X44)|object(X45,X44))|~on(X45,X46,X44))|on(X45,X46,s(X44)))))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,(![X44]:(![X45]:(~nonfixed(X45)|(![X46]:((~a_block(X46)|~neq(X45,X46))|(((~time(X44)|object(X45,X44))|~on(X45,X46,X44))|on(X45,X46,s(X44)))))))),inference(variable_rename,[status(thm)],[c61])).])).
% 0.53/0.70 cnf(c64,plain,~nonfixed(X142)|~a_block(X141)|~neq(X142,X141)|~time(X143)|object(X142,X143)|~on(X142,X141,X143)|on(X142,X141,s(X143)),inference(split_conjunct,[status(thm)],[c63])).
% 0.53/0.70 fof(non_object_remains_not_on,axiom,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&(~object(V,I)))&(~on(V,W,I)))=>(~on(V,W,s(I))))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', non_object_remains_not_on)).
% 0.53/0.70 fof(c51,plain,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&~object(V,I))&~on(V,W,I))=>~on(V,W,s(I)))))))),inference(fof_simplification,[status(thm)],[non_object_remains_not_on])).
% 0.53/0.70 fof(c52,plain,(![I]:(![V]:(~nonfixed(V)|(![W]:((~a_block(W)|~neq(V,W))|(((~time(I)|object(V,I))|on(V,W,I))|~on(V,W,s(I)))))))),inference(fof_nnf,[status(thm)],[c51])).
% 0.53/0.70 fof(c54,plain,(![X39]:(![X40]:(![X41]:(~nonfixed(X40)|((~a_block(X41)|~neq(X40,X41))|(((~time(X39)|object(X40,X39))|on(X40,X41,X39))|~on(X40,X41,s(X39)))))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,(![X39]:(![X40]:(~nonfixed(X40)|(![X41]:((~a_block(X41)|~neq(X40,X41))|(((~time(X39)|object(X40,X39))|on(X40,X41,X39))|~on(X40,X41,s(X39)))))))),inference(variable_rename,[status(thm)],[c52])).])).
% 0.53/0.70 cnf(c55,plain,~nonfixed(X138)|~a_block(X139)|~neq(X138,X139)|~time(X140)|object(X138,X140)|on(X138,X139,X140)|~on(X138,X139,s(X140)),inference(split_conjunct,[status(thm)],[c54])).
% 0.53/0.70 fof(place_object_block_on_destination,axiom,(![I]:(![X]:(nonfixed(X)=>(![Z]:((a_block(Z)&neq(X,Z))=>(((time(I)&object(X,I))&destination(Z,I))=>on(X,Z,s(I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', place_object_block_on_destination)).
% 0.53/0.70 fof(c91,plain,(![I]:(![X]:(~nonfixed(X)|(![Z]:((~a_block(Z)|~neq(X,Z))|(((~time(I)|~object(X,I))|~destination(Z,I))|on(X,Z,s(I)))))))),inference(fof_nnf,[status(thm)],[place_object_block_on_destination])).
% 0.53/0.70 fof(c93,plain,(![X63]:(![X64]:(![X65]:(~nonfixed(X64)|((~a_block(X65)|~neq(X64,X65))|(((~time(X63)|~object(X64,X63))|~destination(X65,X63))|on(X64,X65,s(X63)))))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,(![X63]:(![X64]:(~nonfixed(X64)|(![X65]:((~a_block(X65)|~neq(X64,X65))|(((~time(X63)|~object(X64,X63))|~destination(X65,X63))|on(X64,X65,s(X63)))))))),inference(variable_rename,[status(thm)],[c91])).])).
% 0.53/0.70 cnf(c94,plain,~nonfixed(X136)|~a_block(X135)|~neq(X136,X135)|~time(X137)|~object(X136,X137)|~destination(X135,X137)|on(X136,X135,s(X137)),inference(split_conjunct,[status(thm)],[c93])).
% 0.53/0.70 fof(remove_object_block_from_source,axiom,(![I]:(![X]:(nonfixed(X)=>(![Y]:((a_block(Y)&neq(X,Y))=>(((time(I)&object(X,I))&source(Y,I))=>(~on(X,Y,s(I))))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', remove_object_block_from_source)).
% 0.53/0.70 fof(c86,plain,(![I]:(![X]:(nonfixed(X)=>(![Y]:((a_block(Y)&neq(X,Y))=>(((time(I)&object(X,I))&source(Y,I))=>~on(X,Y,s(I)))))))),inference(fof_simplification,[status(thm)],[remove_object_block_from_source])).
% 0.53/0.70 fof(c87,plain,(![I]:(![X]:(~nonfixed(X)|(![Y]:((~a_block(Y)|~neq(X,Y))|(((~time(I)|~object(X,I))|~source(Y,I))|~on(X,Y,s(I)))))))),inference(fof_nnf,[status(thm)],[c86])).
% 0.53/0.70 fof(c89,plain,(![X60]:(![X61]:(![X62]:(~nonfixed(X61)|((~a_block(X62)|~neq(X61,X62))|(((~time(X60)|~object(X61,X60))|~source(X62,X60))|~on(X61,X62,s(X60)))))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,(![X60]:(![X61]:(~nonfixed(X61)|(![X62]:((~a_block(X62)|~neq(X61,X62))|(((~time(X60)|~object(X61,X60))|~source(X62,X60))|~on(X61,X62,s(X60)))))))),inference(variable_rename,[status(thm)],[c87])).])).
% 0.53/0.70 cnf(c90,plain,~nonfixed(X132)|~a_block(X134)|~neq(X132,X134)|~time(X133)|~object(X132,X133)|~source(X134,X133)|~on(X132,X134,s(X133)),inference(split_conjunct,[status(thm)],[c89])).
% 0.53/0.70 fof(only_one_on,axiom,(![I]:(![X]:(nonfixed(X)=>(![Y]:((nonfixed(Y)&neq(X,Y))=>(![Z]:(((nonfixed(Z)&neq(X,Z))&neq(Y,Z))=>(~(on(X,Y,I)&on(Z,Y,I)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', only_one_on)).
% 0.53/0.70 fof(c13,plain,(![I]:(![X]:(~nonfixed(X)|(![Y]:((~nonfixed(Y)|~neq(X,Y))|(![Z]:(((~nonfixed(Z)|~neq(X,Z))|~neq(Y,Z))|(~on(X,Y,I)|~on(Z,Y,I))))))))),inference(fof_nnf,[status(thm)],[only_one_on])).
% 0.53/0.70 fof(c15,plain,(![X12]:(![X13]:(![X14]:(![X15]:(~nonfixed(X13)|((~nonfixed(X14)|~neq(X13,X14))|(((~nonfixed(X15)|~neq(X13,X15))|~neq(X14,X15))|(~on(X13,X14,X12)|~on(X15,X14,X12))))))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,(![X12]:(![X13]:(~nonfixed(X13)|(![X14]:((~nonfixed(X14)|~neq(X13,X14))|(![X15]:(((~nonfixed(X15)|~neq(X13,X15))|~neq(X14,X15))|(~on(X13,X14,X12)|~on(X15,X14,X12))))))))),inference(variable_rename,[status(thm)],[c13])).])).
% 0.53/0.70 cnf(c16,plain,~nonfixed(X110)|~nonfixed(X108)|~neq(X110,X108)|~nonfixed(X107)|~neq(X110,X107)|~neq(X108,X107)|~on(X110,X108,X109)|~on(X107,X108,X109),inference(split_conjunct,[status(thm)],[c15])).
% 0.53/0.70 cnf(c99,plain,~nonfixed(X129)|~nonfixed(X131)|~neq(X129,X131)|~neq(X129,X129)|~neq(X131,X129)|~on(X129,X131,X130),inference(factor,[status(thm)],[c16])).
% 0.53/0.70 fof(object_block_on_source,axiom,(![I]:(![X]:(nonfixed(X)=>(![Y]:((a_block(Y)&neq(X,Y))=>((object(X,I)&source(Y,I))=>on(X,Y,I))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', object_block_on_source)).
% 0.53/0.70 fof(c75,plain,(![I]:(![X]:(~nonfixed(X)|(![Y]:((~a_block(Y)|~neq(X,Y))|((~object(X,I)|~source(Y,I))|on(X,Y,I))))))),inference(fof_nnf,[status(thm)],[object_block_on_source])).
% 0.53/0.70 fof(c77,plain,(![X53]:(![X54]:(![X55]:(~nonfixed(X54)|((~a_block(X55)|~neq(X54,X55))|((~object(X54,X53)|~source(X55,X53))|on(X54,X55,X53))))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,(![X53]:(![X54]:(~nonfixed(X54)|(![X55]:((~a_block(X55)|~neq(X54,X55))|((~object(X54,X53)|~source(X55,X53))|on(X54,X55,X53))))))),inference(variable_rename,[status(thm)],[c75])).])).
% 0.53/0.70 cnf(c78,plain,~nonfixed(X127)|~a_block(X126)|~neq(X127,X126)|~object(X127,X128)|~source(X126,X128)|on(X127,X126,X128),inference(split_conjunct,[status(thm)],[c77])).
% 0.53/0.70 fof(non_destination_remains_not_on,axiom,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&(~destination(W,I)))&(~on(V,W,I)))=>(~on(V,W,s(I))))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', non_destination_remains_not_on)).
% 0.53/0.70 fof(c46,plain,(![I]:(![V]:(nonfixed(V)=>(![W]:((a_block(W)&neq(V,W))=>(((time(I)&~destination(W,I))&~on(V,W,I))=>~on(V,W,s(I)))))))),inference(fof_simplification,[status(thm)],[non_destination_remains_not_on])).
% 0.53/0.70 fof(c47,plain,(![I]:(![V]:(~nonfixed(V)|(![W]:((~a_block(W)|~neq(V,W))|(((~time(I)|destination(W,I))|on(V,W,I))|~on(V,W,s(I)))))))),inference(fof_nnf,[status(thm)],[c46])).
% 0.53/0.70 fof(c49,plain,(![X36]:(![X37]:(![X38]:(~nonfixed(X37)|((~a_block(X38)|~neq(X37,X38))|(((~time(X36)|destination(X38,X36))|on(X37,X38,X36))|~on(X37,X38,s(X36)))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X36]:(![X37]:(~nonfixed(X37)|(![X38]:((~a_block(X38)|~neq(X37,X38))|(((~time(X36)|destination(X38,X36))|on(X37,X38,X36))|~on(X37,X38,s(X36)))))))),inference(variable_rename,[status(thm)],[c47])).])).
% 0.53/0.70 cnf(c50,plain,~nonfixed(X123)|~a_block(X124)|~neq(X123,X124)|~time(X125)|destination(X124,X125)|on(X123,X124,X125)|~on(X123,X124,s(X125)),inference(split_conjunct,[status(thm)],[c49])).
% 0.53/0.71 fof(non_destination_remains_clear,axiom,(![I]:(![W]:(nonfixed(W)=>(((time(I)&(~destination(W,I)))&clear(W,I))=>clear(W,s(I)))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', non_destination_remains_clear)).
% 0.53/0.71 fof(c65,plain,(![I]:(![W]:(nonfixed(W)=>(((time(I)&~destination(W,I))&clear(W,I))=>clear(W,s(I)))))),inference(fof_simplification,[status(thm)],[non_destination_remains_clear])).
% 0.53/0.71 fof(c66,plain,(![I]:(![W]:(~nonfixed(W)|(((~time(I)|destination(W,I))|~clear(W,I))|clear(W,s(I)))))),inference(fof_nnf,[status(thm)],[c65])).
% 0.53/0.71 fof(c67,plain,(![X47]:(![X48]:(~nonfixed(X48)|(((~time(X47)|destination(X48,X47))|~clear(X48,X47))|clear(X48,s(X47)))))),inference(variable_rename,[status(thm)],[c66])).
% 0.53/0.71 cnf(c68,plain,~nonfixed(X121)|~time(X122)|destination(X121,X122)|~clear(X121,X122)|clear(X121,s(X122)),inference(split_conjunct,[status(thm)],[c67])).
% 0.53/0.71 fof(non_source_remains_not_clear,axiom,(![I]:(![W]:(nonfixed(W)=>(((time(I)&(~source(W,I)))&(~clear(W,I)))=>(~clear(W,s(I))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', non_source_remains_not_clear)).
% 0.53/0.71 fof(c56,plain,(![I]:(![W]:(nonfixed(W)=>(((time(I)&~source(W,I))&~clear(W,I))=>~clear(W,s(I)))))),inference(fof_simplification,[status(thm)],[non_source_remains_not_clear])).
% 0.53/0.71 fof(c57,plain,(![I]:(![W]:(~nonfixed(W)|(((~time(I)|source(W,I))|clear(W,I))|~clear(W,s(I)))))),inference(fof_nnf,[status(thm)],[c56])).
% 0.53/0.71 fof(c58,plain,(![X42]:(![X43]:(~nonfixed(X43)|(((~time(X42)|source(X43,X42))|clear(X43,X42))|~clear(X43,s(X42)))))),inference(variable_rename,[status(thm)],[c57])).
% 0.53/0.71 cnf(c59,plain,~nonfixed(X120)|~time(X119)|source(X120,X119)|clear(X120,X119)|~clear(X120,s(X119)),inference(split_conjunct,[status(thm)],[c58])).
% 0.53/0.71 fof(not_on_each_other,axiom,(![I]:(![X]:(a_block(X)=>(![Y]:((a_block(Y)&neq(X,Y))=>(~(on(X,Y,I)&on(Y,X,I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', not_on_each_other)).
% 0.53/0.71 fof(c21,plain,(![I]:(![X]:(~a_block(X)|(![Y]:((~a_block(Y)|~neq(X,Y))|(~on(X,Y,I)|~on(Y,X,I))))))),inference(fof_nnf,[status(thm)],[not_on_each_other])).
% 0.53/0.71 fof(c23,plain,(![X18]:(![X19]:(![X20]:(~a_block(X19)|((~a_block(X20)|~neq(X19,X20))|(~on(X19,X20,X18)|~on(X20,X19,X18))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,(![X18]:(![X19]:(~a_block(X19)|(![X20]:((~a_block(X20)|~neq(X19,X20))|(~on(X19,X20,X18)|~on(X20,X19,X18))))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.53/0.71 cnf(c24,plain,~a_block(X114)|~a_block(X115)|~neq(X114,X115)|~on(X114,X115,X116)|~on(X115,X114,X116),inference(split_conjunct,[status(thm)],[c23])).
% 0.53/0.71 fof(only_on_one_thing,axiom,(![I]:(![X]:(nonfixed(X)=>(![Y]:((a_block(Y)&neq(X,Y))=>(![Z]:(((a_block(Z)&neq(X,Z))&neq(Y,Z))=>(~(on(X,Y,I)&on(X,Z,I)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', only_on_one_thing)).
% 0.53/0.71 fof(c9,plain,(![I]:(![X]:(~nonfixed(X)|(![Y]:((~a_block(Y)|~neq(X,Y))|(![Z]:(((~a_block(Z)|~neq(X,Z))|~neq(Y,Z))|(~on(X,Y,I)|~on(X,Z,I))))))))),inference(fof_nnf,[status(thm)],[only_on_one_thing])).
% 0.53/0.71 fof(c11,plain,(![X8]:(![X9]:(![X10]:(![X11]:(~nonfixed(X9)|((~a_block(X10)|~neq(X9,X10))|(((~a_block(X11)|~neq(X9,X11))|~neq(X10,X11))|(~on(X9,X10,X8)|~on(X9,X11,X8))))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,(![X8]:(![X9]:(~nonfixed(X9)|(![X10]:((~a_block(X10)|~neq(X9,X10))|(![X11]:(((~a_block(X11)|~neq(X9,X11))|~neq(X10,X11))|(~on(X9,X10,X8)|~on(X9,X11,X8))))))))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.53/0.71 cnf(c12,plain,~nonfixed(X94)|~a_block(X92)|~neq(X94,X92)|~a_block(X91)|~neq(X94,X91)|~neq(X92,X91)|~on(X94,X92,X93)|~on(X94,X91,X93),inference(split_conjunct,[status(thm)],[c11])).
% 0.53/0.71 cnf(c96,plain,~nonfixed(X113)|~a_block(X112)|~neq(X113,X112)|~neq(X112,X112)|~on(X113,X112,X111),inference(factor,[status(thm)],[c12])).
% 0.53/0.71 fof(only_one_object_block,axiom,(![I]:(![X1]:(nonfixed(X1)=>(![X2]:((a_block(X2)&neq(X1,X2))=>(~(object(X1,I)&object(X2,I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', only_one_object_block)).
% 0.53/0.71 fof(c42,plain,(![I]:(![X1]:(~nonfixed(X1)|(![X2]:((~a_block(X2)|~neq(X1,X2))|(~object(X1,I)|~object(X2,I))))))),inference(fof_nnf,[status(thm)],[only_one_object_block])).
% 0.53/0.71 fof(c44,plain,(![X33]:(![X34]:(![X35]:(~nonfixed(X34)|((~a_block(X35)|~neq(X34,X35))|(~object(X34,X33)|~object(X35,X33))))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,(![X33]:(![X34]:(~nonfixed(X34)|(![X35]:((~a_block(X35)|~neq(X34,X35))|(~object(X34,X33)|~object(X35,X33))))))),inference(variable_rename,[status(thm)],[c42])).])).
% 0.53/0.71 cnf(c45,plain,~nonfixed(X103)|~a_block(X102)|~neq(X103,X102)|~object(X103,X104)|~object(X102,X104),inference(split_conjunct,[status(thm)],[c44])).
% 0.53/0.71 cnf(c98,plain,~nonfixed(X106)|~a_block(X106)|~neq(X106,X106)|~object(X106,X105),inference(factor,[status(thm)],[c45])).
% 0.53/0.71 fof(only_one_source_block,axiom,(![I]:(![Y1]:(a_block(Y1)=>(![Y2]:((a_block(Y2)&neq(Y1,Y2))=>(~(source(Y1,I)&source(Y2,I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', only_one_source_block)).
% 0.53/0.71 fof(c38,plain,(![I]:(![Y1]:(~a_block(Y1)|(![Y2]:((~a_block(Y2)|~neq(Y1,Y2))|(~source(Y1,I)|~source(Y2,I))))))),inference(fof_nnf,[status(thm)],[only_one_source_block])).
% 0.53/0.71 fof(c40,plain,(![X30]:(![X31]:(![X32]:(~a_block(X31)|((~a_block(X32)|~neq(X31,X32))|(~source(X31,X30)|~source(X32,X30))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X30]:(![X31]:(~a_block(X31)|(![X32]:((~a_block(X32)|~neq(X31,X32))|(~source(X31,X30)|~source(X32,X30))))))),inference(variable_rename,[status(thm)],[c38])).])).
% 0.53/0.71 cnf(c41,plain,~a_block(X97)|~a_block(X99)|~neq(X97,X99)|~source(X97,X98)|~source(X99,X98),inference(split_conjunct,[status(thm)],[c40])).
% 0.53/0.71 cnf(c97,plain,~a_block(X101)|~neq(X101,X101)|~source(X101,X100),inference(factor,[status(thm)],[c41])).
% 0.53/0.71 fof(only_one_destination_block,axiom,(![I]:(![Z1]:(a_block(Z1)=>(![Z2]:((a_block(Z2)&neq(Z1,Z2))=>(~(destination(Z1,I)&destination(Z2,I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', only_one_destination_block)).
% 0.53/0.71 fof(c34,plain,(![I]:(![Z1]:(~a_block(Z1)|(![Z2]:((~a_block(Z2)|~neq(Z1,Z2))|(~destination(Z1,I)|~destination(Z2,I))))))),inference(fof_nnf,[status(thm)],[only_one_destination_block])).
% 0.53/0.71 fof(c36,plain,(![X27]:(![X28]:(![X29]:(~a_block(X28)|((~a_block(X29)|~neq(X28,X29))|(~destination(X28,X27)|~destination(X29,X27))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X27]:(![X28]:(~a_block(X28)|(![X29]:((~a_block(X29)|~neq(X28,X29))|(~destination(X28,X27)|~destination(X29,X27))))))),inference(variable_rename,[status(thm)],[c34])).])).
% 0.53/0.71 cnf(c37,plain,~a_block(X88)|~a_block(X89)|~neq(X88,X89)|~destination(X88,X90)|~destination(X89,X90),inference(split_conjunct,[status(thm)],[c36])).
% 0.53/0.71 cnf(c95,plain,~a_block(X95)|~neq(X95,X95)|~destination(X95,X96),inference(factor,[status(thm)],[c37])).
% 0.53/0.71 fof(clear_source_after_removal,axiom,(![I]:(![Y]:(nonfixed(Y)=>((time(I)&source(Y,I))=>clear(Y,s(I)))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', clear_source_after_removal)).
% 0.53/0.71 fof(c83,plain,(![I]:(![Y]:(~nonfixed(Y)|((~time(I)|~source(Y,I))|clear(Y,s(I)))))),inference(fof_nnf,[status(thm)],[clear_source_after_removal])).
% 0.53/0.71 fof(c84,plain,(![X58]:(![X59]:(~nonfixed(X59)|((~time(X58)|~source(X59,X58))|clear(X59,s(X58)))))),inference(variable_rename,[status(thm)],[c83])).
% 0.53/0.71 cnf(c85,plain,~nonfixed(X87)|~time(X86)|~source(X87,X86)|clear(X87,s(X86)),inference(split_conjunct,[status(thm)],[c84])).
% 0.53/0.71 fof(not_clear_destination_after_placement,axiom,(![I]:(![Z]:(nonfixed(Z)=>((time(I)&destination(Z,I))=>(~clear(Z,s(I))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', not_clear_destination_after_placement)).
% 0.53/0.71 fof(c79,plain,(![I]:(![Z]:(nonfixed(Z)=>((time(I)&destination(Z,I))=>~clear(Z,s(I)))))),inference(fof_simplification,[status(thm)],[not_clear_destination_after_placement])).
% 0.53/0.71 fof(c80,plain,(![I]:(![Z]:(~nonfixed(Z)|((~time(I)|~destination(Z,I))|~clear(Z,s(I)))))),inference(fof_nnf,[status(thm)],[c79])).
% 0.53/0.71 fof(c81,plain,(![X56]:(![X57]:(~nonfixed(X57)|((~time(X56)|~destination(X57,X56))|~clear(X57,s(X56)))))),inference(variable_rename,[status(thm)],[c80])).
% 0.53/0.71 cnf(c82,plain,~nonfixed(X85)|~time(X84)|~destination(X85,X84)|~clear(X85,s(X84)),inference(split_conjunct,[status(thm)],[c81])).
% 0.53/0.71 fof(object_block_is_clear,axiom,(![I]:(![X]:(nonfixed(X)=>(object(X,I)=>clear(X,I))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', object_block_is_clear)).
% 0.53/0.71 fof(c72,plain,(![I]:(![X]:(~nonfixed(X)|(~object(X,I)|clear(X,I))))),inference(fof_nnf,[status(thm)],[object_block_is_clear])).
% 0.53/0.71 fof(c73,plain,(![X51]:(![X52]:(~nonfixed(X52)|(~object(X52,X51)|clear(X52,X51))))),inference(variable_rename,[status(thm)],[c72])).
% 0.53/0.71 cnf(c74,plain,~nonfixed(X82)|~object(X82,X83)|clear(X82,X83),inference(split_conjunct,[status(thm)],[c73])).
% 0.53/0.71 fof(destination_block_is_clear,axiom,(![I]:(![Z]:(nonfixed(Z)=>(destination(Z,I)=>clear(Z,I))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', destination_block_is_clear)).
% 0.53/0.71 fof(c69,plain,(![I]:(![Z]:(~nonfixed(Z)|(~destination(Z,I)|clear(Z,I))))),inference(fof_nnf,[status(thm)],[destination_block_is_clear])).
% 0.53/0.71 fof(c70,plain,(![X49]:(![X50]:(~nonfixed(X50)|(~destination(X50,X49)|clear(X50,X49))))),inference(variable_rename,[status(thm)],[c69])).
% 0.53/0.71 cnf(c71,plain,~nonfixed(X80)|~destination(X80,X81)|clear(X80,X81),inference(split_conjunct,[status(thm)],[c70])).
% 0.53/0.71 fof(not_clear_if_something_on,axiom,(![I]:(![X]:(nonfixed(X)=>(![Y]:(nonfixed(Y)=>(~(on(X,Y,I)&clear(Y,I)))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', not_clear_if_something_on)).
% 0.53/0.71 fof(c5,plain,(![I]:(![X]:(~nonfixed(X)|(![Y]:(~nonfixed(Y)|(~on(X,Y,I)|~clear(Y,I))))))),inference(fof_nnf,[status(thm)],[not_clear_if_something_on])).
% 0.53/0.71 fof(c7,plain,(![X5]:(![X6]:(![X7]:(~nonfixed(X6)|(~nonfixed(X7)|(~on(X6,X7,X5)|~clear(X7,X5))))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,(![X5]:(![X6]:(~nonfixed(X6)|(![X7]:(~nonfixed(X7)|(~on(X6,X7,X5)|~clear(X7,X5))))))),inference(variable_rename,[status(thm)],[c5])).])).
% 0.53/0.71 cnf(c8,plain,~nonfixed(X77)|~nonfixed(X79)|~on(X77,X79,X78)|~clear(X79,X78),inference(split_conjunct,[status(thm)],[c7])).
% 0.53/0.71 fof(object_is_not_source,axiom,(![I]:(![X]:(nonfixed(X)=>(~(object(X,I)&source(X,I)))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', object_is_not_source)).
% 0.53/0.71 fof(c31,plain,(![I]:(![X]:(~nonfixed(X)|(~object(X,I)|~source(X,I))))),inference(fof_nnf,[status(thm)],[object_is_not_source])).
% 0.53/0.71 fof(c32,plain,(![X25]:(![X26]:(~nonfixed(X26)|(~object(X26,X25)|~source(X26,X25))))),inference(variable_rename,[status(thm)],[c31])).
% 0.53/0.71 cnf(c33,plain,~nonfixed(X76)|~object(X76,X75)|~source(X76,X75),inference(split_conjunct,[status(thm)],[c32])).
% 0.53/0.71 fof(object_is_not_destination,axiom,(![I]:(![X]:(nonfixed(X)=>(~(object(X,I)&destination(X,I)))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', object_is_not_destination)).
% 0.53/0.71 fof(c28,plain,(![I]:(![X]:(~nonfixed(X)|(~object(X,I)|~destination(X,I))))),inference(fof_nnf,[status(thm)],[object_is_not_destination])).
% 0.53/0.71 fof(c29,plain,(![X23]:(![X24]:(~nonfixed(X24)|(~object(X24,X23)|~destination(X24,X23))))),inference(variable_rename,[status(thm)],[c28])).
% 0.53/0.71 cnf(c30,plain,~nonfixed(X73)|~object(X73,X74)|~destination(X73,X74),inference(split_conjunct,[status(thm)],[c29])).
% 0.53/0.71 fof(source_is_not_destination,axiom,(![I]:(![Y]:(a_block(Y)=>(~(source(Y,I)&destination(Y,I)))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', source_is_not_destination)).
% 0.53/0.71 fof(c25,plain,(![I]:(![Y]:(~a_block(Y)|(~source(Y,I)|~destination(Y,I))))),inference(fof_nnf,[status(thm)],[source_is_not_destination])).
% 0.53/0.71 fof(c26,plain,(![X21]:(![X22]:(~a_block(X22)|(~source(X22,X21)|~destination(X22,X21))))),inference(variable_rename,[status(thm)],[c25])).
% 0.53/0.71 cnf(c27,plain,~a_block(X71)|~source(X71,X72)|~destination(X71,X72),inference(split_conjunct,[status(thm)],[c26])).
% 0.53/0.71 fof(fixed_not_on_anything,axiom,(![I]:(![X]:(a_block(X)=>(![Y]:(fixed(Y)=>(~on(Y,X,I))))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', fixed_not_on_anything)).
% 0.53/0.71 fof(c0,plain,(![I]:(![X]:(a_block(X)=>(![Y]:(fixed(Y)=>~on(Y,X,I)))))),inference(fof_simplification,[status(thm)],[fixed_not_on_anything])).
% 0.53/0.71 fof(c1,plain,(![I]:(![X]:(~a_block(X)|(![Y]:(~fixed(Y)|~on(Y,X,I)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.53/0.71 fof(c3,plain,(![X2]:(![X3]:(![X4]:(~a_block(X3)|(~fixed(X4)|~on(X4,X3,X2)))))),inference(shift_quantors,[status(thm)],[fof(c2,plain,(![X2]:(![X3]:(~a_block(X3)|(![X4]:(~fixed(X4)|~on(X4,X3,X2)))))),inference(variable_rename,[status(thm)],[c1])).])).
% 0.53/0.71 cnf(c4,plain,~a_block(X69)|~fixed(X68)|~on(X68,X69,X70),inference(split_conjunct,[status(thm)],[c3])).
% 0.53/0.71 fof(not_on_self,axiom,(![I]:(![X]:(a_block(X)=>(~on(X,X,I))))),file('/export/starexec/sandbox/benchmark/Axioms/PLA002+0.ax', not_on_self)).
% 0.53/0.71 fof(c17,plain,(![I]:(![X]:(a_block(X)=>~on(X,X,I)))),inference(fof_simplification,[status(thm)],[not_on_self])).
% 0.53/0.71 fof(c18,plain,(![I]:(![X]:(~a_block(X)|~on(X,X,I)))),inference(fof_nnf,[status(thm)],[c17])).
% 0.53/0.71 fof(c19,plain,(![X16]:(![X17]:(~a_block(X17)|~on(X17,X17,X16)))),inference(variable_rename,[status(thm)],[c18])).
% 0.53/0.71 cnf(c20,plain,~a_block(X67)|~on(X67,X67,X66),inference(split_conjunct,[status(thm)],[c19])).
% 0.53/0.71 % SZS output end Saturation
% 0.53/0.71
% 0.53/0.71 % Initial clauses : 24
% 0.53/0.71 % Processed clauses : 29
% 0.53/0.71 % Factors computed : 6
% 0.53/0.71 % Resolvents computed: 0
% 0.53/0.71 % Tautologies deleted: 0
% 0.53/0.71 % Forward subsumed : 1
% 0.53/0.71 % Backward subsumed : 0
% 0.53/0.71 % -------- CPU Time ---------
% 0.53/0.71 % User time : 0.314 s
% 0.53/0.71 % System time : 0.024 s
% 0.53/0.71 % Total time : 0.338 s
%------------------------------------------------------------------------------