%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR154+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:19:28 EDT 2024
% Result : Satisfiable 0.41s 0.58s
% Output : Saturation 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : CSR154+1 : TPTP v8.1.2. Released v6.4.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 01:16:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.41/0.58 % Version: 1.5
% 0.41/0.58 % SZS status Satisfiable
% 0.41/0.58 % SZS output start Saturation
% 0.41/0.58 fof(change_holding,axiom,(![Event]:(![Time]:(![Fluent]:(![Fluent2]:(![Offset]:(((((happens(Event,Time)&initiates(Event,Fluent,Time))&less(n0,Offset))&trajectory(Fluent,Time,Fluent2,Offset))&(~stoppedIn(Time,Fluent,plus(Time,Offset))))=>holdsAt(Fluent2,plus(Time,Offset)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', change_holding)).
% 0.41/0.58 fof(c47,plain,(![Event]:(![Time]:(![Fluent]:(![Fluent2]:(![Offset]:(((((happens(Event,Time)&initiates(Event,Fluent,Time))&less(n0,Offset))&trajectory(Fluent,Time,Fluent2,Offset))&~stoppedIn(Time,Fluent,plus(Time,Offset)))=>holdsAt(Fluent2,plus(Time,Offset)))))))),inference(fof_simplification,[status(thm)],[change_holding])).
% 0.41/0.58 fof(c48,plain,(![Event]:(![Time]:(![Fluent]:(![Fluent2]:(![Offset]:(((((~happens(Event,Time)|~initiates(Event,Fluent,Time))|~less(n0,Offset))|~trajectory(Fluent,Time,Fluent2,Offset))|stoppedIn(Time,Fluent,plus(Time,Offset)))|holdsAt(Fluent2,plus(Time,Offset)))))))),inference(fof_nnf,[status(thm)],[c47])).
% 0.41/0.58 fof(c49,plain,(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(((((~happens(X31,X32)|~initiates(X31,X33,X32))|~less(n0,X35))|~trajectory(X33,X32,X34,X35))|stoppedIn(X32,X33,plus(X32,X35)))|holdsAt(X34,plus(X32,X35)))))))),inference(variable_rename,[status(thm)],[c48])).
% 0.41/0.58 cnf(c50,plain,~happens(X130,X126)|~initiates(X130,X128,X126)|~less(n0,X129)|~trajectory(X128,X126,X127,X129)|stoppedIn(X126,X128,plus(X126,X129))|holdsAt(X127,plus(X126,X129)),inference(split_conjunct,[status(thm)],[c49])).
% 0.41/0.58 fof(antitrajectory,axiom,(![Event]:(![Time1]:(![Fluent1]:(![Time2]:(![Fluent2]:(((((happens(Event,Time1)&terminates(Event,Fluent1,Time1))&less(n0,Time2))&antitrajectory(Fluent1,Time1,Fluent2,Time2))&(~startedIn(Time1,Fluent1,plus(Time1,Time2))))=>holdsAt(Fluent2,plus(Time1,Time2)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', antitrajectory)).
% 0.41/0.58 fof(c43,plain,(![Event]:(![Time1]:(![Fluent1]:(![Time2]:(![Fluent2]:(((((happens(Event,Time1)&terminates(Event,Fluent1,Time1))&less(n0,Time2))&antitrajectory(Fluent1,Time1,Fluent2,Time2))&~startedIn(Time1,Fluent1,plus(Time1,Time2)))=>holdsAt(Fluent2,plus(Time1,Time2)))))))),inference(fof_simplification,[status(thm)],[antitrajectory])).
% 0.41/0.58 fof(c44,plain,(![Event]:(![Time1]:(![Fluent1]:(![Time2]:(![Fluent2]:(((((~happens(Event,Time1)|~terminates(Event,Fluent1,Time1))|~less(n0,Time2))|~antitrajectory(Fluent1,Time1,Fluent2,Time2))|startedIn(Time1,Fluent1,plus(Time1,Time2)))|holdsAt(Fluent2,plus(Time1,Time2)))))))),inference(fof_nnf,[status(thm)],[c43])).
% 0.41/0.58 fof(c45,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(((((~happens(X26,X27)|~terminates(X26,X28,X27))|~less(n0,X29))|~antitrajectory(X28,X27,X30,X29))|startedIn(X27,X28,plus(X27,X29)))|holdsAt(X30,plus(X27,X29)))))))),inference(variable_rename,[status(thm)],[c44])).
% 0.41/0.58 cnf(c46,plain,~happens(X122,X121)|~terminates(X122,X125,X121)|~less(n0,X123)|~antitrajectory(X125,X121,X124,X123)|startedIn(X121,X125,plus(X121,X123))|holdsAt(X124,plus(X121,X123)),inference(split_conjunct,[status(thm)],[c45])).
% 0.41/0.58 fof(keep_holding,axiom,(![Fluent]:(![Time]:(((holdsAt(Fluent,Time)&(~releasedAt(Fluent,plus(Time,n1))))&(~(?[Event]:(happens(Event,Time)&terminates(Event,Fluent,Time)))))=>holdsAt(Fluent,plus(Time,n1))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', keep_holding)).
% 0.41/0.58 fof(c36,plain,(![Fluent]:(![Time]:(((holdsAt(Fluent,Time)&~releasedAt(Fluent,plus(Time,n1)))&(~(?[Event]:(happens(Event,Time)&terminates(Event,Fluent,Time)))))=>holdsAt(Fluent,plus(Time,n1))))),inference(fof_simplification,[status(thm)],[keep_holding])).
% 0.41/0.58 fof(c37,plain,(![Fluent]:(![Time]:(((~holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]:(happens(Event,Time)&terminates(Event,Fluent,Time))))|holdsAt(Fluent,plus(Time,n1))))),inference(fof_nnf,[status(thm)],[c36])).
% 0.41/0.58 fof(c38,plain,(![X23]:(![X24]:(((~holdsAt(X23,X24)|releasedAt(X23,plus(X24,n1)))|(?[X25]:(happens(X25,X24)&terminates(X25,X23,X24))))|holdsAt(X23,plus(X24,n1))))),inference(variable_rename,[status(thm)],[c37])).
% 0.41/0.58 fof(c39,plain,(![X23]:(![X24]:(((~holdsAt(X23,X24)|releasedAt(X23,plus(X24,n1)))|(happens(skolem0004(X23,X24),X24)&terminates(skolem0004(X23,X24),X23,X24)))|holdsAt(X23,plus(X24,n1))))),inference(skolemize,[status(esa)],[c38])).
% 0.41/0.58 fof(c40,plain,(![X23]:(![X24]:((((~holdsAt(X23,X24)|releasedAt(X23,plus(X24,n1)))|happens(skolem0004(X23,X24),X24))|holdsAt(X23,plus(X24,n1)))&(((~holdsAt(X23,X24)|releasedAt(X23,plus(X24,n1)))|terminates(skolem0004(X23,X24),X23,X24))|holdsAt(X23,plus(X24,n1)))))),inference(distribute,[status(thm)],[c39])).
% 0.41/0.58 cnf(c42,plain,~holdsAt(X119,X120)|releasedAt(X119,plus(X120,n1))|terminates(skolem0004(X119,X120),X119,X120)|holdsAt(X119,plus(X120,n1)),inference(split_conjunct,[status(thm)],[c40])).
% 0.41/0.58 fof(keep_not_holding,axiom,(![Fluent]:(![Time]:((((~holdsAt(Fluent,Time))&(~releasedAt(Fluent,plus(Time,n1))))&(~(?[Event]:(happens(Event,Time)&initiates(Event,Fluent,Time)))))=>(~holdsAt(Fluent,plus(Time,n1)))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', keep_not_holding)).
% 0.41/0.58 fof(c29,plain,(![Fluent]:(![Time]:(((~holdsAt(Fluent,Time)&~releasedAt(Fluent,plus(Time,n1)))&(~(?[Event]:(happens(Event,Time)&initiates(Event,Fluent,Time)))))=>~holdsAt(Fluent,plus(Time,n1))))),inference(fof_simplification,[status(thm)],[keep_not_holding])).
% 0.41/0.58 fof(c30,plain,(![Fluent]:(![Time]:(((holdsAt(Fluent,Time)|releasedAt(Fluent,plus(Time,n1)))|(?[Event]:(happens(Event,Time)&initiates(Event,Fluent,Time))))|~holdsAt(Fluent,plus(Time,n1))))),inference(fof_nnf,[status(thm)],[c29])).
% 0.41/0.58 fof(c31,plain,(![X20]:(![X21]:(((holdsAt(X20,X21)|releasedAt(X20,plus(X21,n1)))|(?[X22]:(happens(X22,X21)&initiates(X22,X20,X21))))|~holdsAt(X20,plus(X21,n1))))),inference(variable_rename,[status(thm)],[c30])).
% 0.41/0.58 fof(c32,plain,(![X20]:(![X21]:(((holdsAt(X20,X21)|releasedAt(X20,plus(X21,n1)))|(happens(skolem0003(X20,X21),X21)&initiates(skolem0003(X20,X21),X20,X21)))|~holdsAt(X20,plus(X21,n1))))),inference(skolemize,[status(esa)],[c31])).
% 0.41/0.58 fof(c33,plain,(![X20]:(![X21]:((((holdsAt(X20,X21)|releasedAt(X20,plus(X21,n1)))|happens(skolem0003(X20,X21),X21))|~holdsAt(X20,plus(X21,n1)))&(((holdsAt(X20,X21)|releasedAt(X20,plus(X21,n1)))|initiates(skolem0003(X20,X21),X20,X21))|~holdsAt(X20,plus(X21,n1)))))),inference(distribute,[status(thm)],[c32])).
% 0.41/0.58 cnf(c35,plain,holdsAt(X117,X118)|releasedAt(X117,plus(X118,n1))|initiates(skolem0003(X117,X118),X117,X118)|~holdsAt(X117,plus(X118,n1)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.58 cnf(c41,plain,~holdsAt(X115,X116)|releasedAt(X115,plus(X116,n1))|happens(skolem0004(X115,X116),X116)|holdsAt(X115,plus(X116,n1)),inference(split_conjunct,[status(thm)],[c40])).
% 0.41/0.58 cnf(c34,plain,holdsAt(X113,X114)|releasedAt(X113,plus(X114,n1))|happens(skolem0003(X113,X114),X114)|~holdsAt(X113,plus(X114,n1)),inference(split_conjunct,[status(thm)],[c33])).
% 0.41/0.58 fof(stoppedin_defn,axiom,(![Time1]:(![Fluent]:(![Time2]:(stoppedIn(Time1,Fluent,Time2)<=>(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&terminates(Event,Fluent,Time)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', stoppedin_defn)).
% 0.41/0.58 fof(c62,plain,(![Time1]:(![Fluent]:(![Time2]:((~stoppedIn(Time1,Fluent,Time2)|(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&terminates(Event,Fluent,Time)))))&((![Event]:(![Time]:(((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~terminates(Event,Fluent,Time))))|stoppedIn(Time1,Fluent,Time2)))))),inference(fof_nnf,[status(thm)],[stoppedin_defn])).
% 0.41/0.58 fof(c63,plain,((![Time1]:(![Fluent]:(![Time2]:(~stoppedIn(Time1,Fluent,Time2)|(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&terminates(Event,Fluent,Time))))))))&(![Time1]:(![Fluent]:(![Time2]:((![Event]:(![Time]:(((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~terminates(Event,Fluent,Time))))|stoppedIn(Time1,Fluent,Time2)))))),inference(shift_quantors,[status(thm)],[c62])).
% 0.41/0.58 fof(c64,plain,((![X46]:(![X47]:(![X48]:(~stoppedIn(X46,X47,X48)|(?[X49]:(?[X50]:(((happens(X49,X50)&less(X46,X50))&less(X50,X48))&terminates(X49,X47,X50))))))))&(![X51]:(![X52]:(![X53]:((![X54]:(![X55]:(((~happens(X54,X55)|~less(X51,X55))|~less(X55,X53))|~terminates(X54,X52,X55))))|stoppedIn(X51,X52,X53)))))),inference(variable_rename,[status(thm)],[c63])).
% 0.41/0.58 fof(c66,plain,(![X46]:(![X47]:(![X48]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~stoppedIn(X46,X47,X48)|(((happens(skolem0007(X46,X47,X48),skolem0008(X46,X47,X48))&less(X46,skolem0008(X46,X47,X48)))&less(skolem0008(X46,X47,X48),X48))&terminates(skolem0007(X46,X47,X48),X47,skolem0008(X46,X47,X48))))&((((~happens(X54,X55)|~less(X51,X55))|~less(X55,X53))|~terminates(X54,X52,X55))|stoppedIn(X51,X52,X53))))))))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X46]:(![X47]:(![X48]:(~stoppedIn(X46,X47,X48)|(((happens(skolem0007(X46,X47,X48),skolem0008(X46,X47,X48))&less(X46,skolem0008(X46,X47,X48)))&less(skolem0008(X46,X47,X48),X48))&terminates(skolem0007(X46,X47,X48),X47,skolem0008(X46,X47,X48)))))))&(![X51]:(![X52]:(![X53]:((![X54]:(![X55]:(((~happens(X54,X55)|~less(X51,X55))|~less(X55,X53))|~terminates(X54,X52,X55))))|stoppedIn(X51,X52,X53)))))),inference(skolemize,[status(esa)],[c64])).])).
% 0.41/0.58 fof(c67,plain,(![X46]:(![X47]:(![X48]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(((((~stoppedIn(X46,X47,X48)|happens(skolem0007(X46,X47,X48),skolem0008(X46,X47,X48)))&(~stoppedIn(X46,X47,X48)|less(X46,skolem0008(X46,X47,X48))))&(~stoppedIn(X46,X47,X48)|less(skolem0008(X46,X47,X48),X48)))&(~stoppedIn(X46,X47,X48)|terminates(skolem0007(X46,X47,X48),X47,skolem0008(X46,X47,X48))))&((((~happens(X54,X55)|~less(X51,X55))|~less(X55,X53))|~terminates(X54,X52,X55))|stoppedIn(X51,X52,X53))))))))))),inference(distribute,[status(thm)],[c66])).
% 0.41/0.58 cnf(c72,plain,~happens(X111,X110)|~less(X108,X110)|~less(X110,X109)|~terminates(X111,X112,X110)|stoppedIn(X108,X112,X109),inference(split_conjunct,[status(thm)],[c67])).
% 0.41/0.58 fof(keep_released,axiom,(![Fluent]:(![Time]:((releasedAt(Fluent,Time)&(~(?[Event]:(happens(Event,Time)&(initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time))))))=>releasedAt(Fluent,plus(Time,n1))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', keep_released)).
% 0.41/0.58 fof(c23,plain,(![Fluent]:(![Time]:((~releasedAt(Fluent,Time)|(?[Event]:(happens(Event,Time)&(initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time)))))|releasedAt(Fluent,plus(Time,n1))))),inference(fof_nnf,[status(thm)],[keep_released])).
% 0.41/0.58 fof(c24,plain,(![X17]:(![X18]:((~releasedAt(X17,X18)|(?[X19]:(happens(X19,X18)&(initiates(X19,X17,X18)|terminates(X19,X17,X18)))))|releasedAt(X17,plus(X18,n1))))),inference(variable_rename,[status(thm)],[c23])).
% 0.41/0.58 fof(c25,plain,(![X17]:(![X18]:((~releasedAt(X17,X18)|(happens(skolem0002(X17,X18),X18)&(initiates(skolem0002(X17,X18),X17,X18)|terminates(skolem0002(X17,X18),X17,X18))))|releasedAt(X17,plus(X18,n1))))),inference(skolemize,[status(esa)],[c24])).
% 0.41/0.58 fof(c26,plain,(![X17]:(![X18]:(((~releasedAt(X17,X18)|happens(skolem0002(X17,X18),X18))|releasedAt(X17,plus(X18,n1)))&((~releasedAt(X17,X18)|(initiates(skolem0002(X17,X18),X17,X18)|terminates(skolem0002(X17,X18),X17,X18)))|releasedAt(X17,plus(X18,n1)))))),inference(distribute,[status(thm)],[c25])).
% 0.41/0.58 cnf(c28,plain,~releasedAt(X107,X106)|initiates(skolem0002(X107,X106),X107,X106)|terminates(skolem0002(X107,X106),X107,X106)|releasedAt(X107,plus(X106,n1)),inference(split_conjunct,[status(thm)],[c26])).
% 0.41/0.58 fof(startedin_defn,axiom,(![Time1]:(![Time2]:(![Fluent]:(startedIn(Time1,Fluent,Time2)<=>(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&initiates(Event,Fluent,Time)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', startedin_defn)).
% 0.41/0.58 fof(c51,plain,(![Time1]:(![Time2]:(![Fluent]:((~startedIn(Time1,Fluent,Time2)|(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&initiates(Event,Fluent,Time)))))&((![Event]:(![Time]:(((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~initiates(Event,Fluent,Time))))|startedIn(Time1,Fluent,Time2)))))),inference(fof_nnf,[status(thm)],[startedin_defn])).
% 0.41/0.58 fof(c52,plain,((![Time1]:(![Time2]:(![Fluent]:(~startedIn(Time1,Fluent,Time2)|(?[Event]:(?[Time]:(((happens(Event,Time)&less(Time1,Time))&less(Time,Time2))&initiates(Event,Fluent,Time))))))))&(![Time1]:(![Time2]:(![Fluent]:((![Event]:(![Time]:(((~happens(Event,Time)|~less(Time1,Time))|~less(Time,Time2))|~initiates(Event,Fluent,Time))))|startedIn(Time1,Fluent,Time2)))))),inference(shift_quantors,[status(thm)],[c51])).
% 0.41/0.58 fof(c53,plain,((![X36]:(![X37]:(![X38]:(~startedIn(X36,X38,X37)|(?[X39]:(?[X40]:(((happens(X39,X40)&less(X36,X40))&less(X40,X37))&initiates(X39,X38,X40))))))))&(![X41]:(![X42]:(![X43]:((![X44]:(![X45]:(((~happens(X44,X45)|~less(X41,X45))|~less(X45,X42))|~initiates(X44,X43,X45))))|startedIn(X41,X43,X42)))))),inference(variable_rename,[status(thm)],[c52])).
% 0.41/0.58 fof(c55,plain,(![X36]:(![X37]:(![X38]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:((~startedIn(X36,X38,X37)|(((happens(skolem0005(X36,X37,X38),skolem0006(X36,X37,X38))&less(X36,skolem0006(X36,X37,X38)))&less(skolem0006(X36,X37,X38),X37))&initiates(skolem0005(X36,X37,X38),X38,skolem0006(X36,X37,X38))))&((((~happens(X44,X45)|~less(X41,X45))|~less(X45,X42))|~initiates(X44,X43,X45))|startedIn(X41,X43,X42))))))))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X36]:(![X37]:(![X38]:(~startedIn(X36,X38,X37)|(((happens(skolem0005(X36,X37,X38),skolem0006(X36,X37,X38))&less(X36,skolem0006(X36,X37,X38)))&less(skolem0006(X36,X37,X38),X37))&initiates(skolem0005(X36,X37,X38),X38,skolem0006(X36,X37,X38)))))))&(![X41]:(![X42]:(![X43]:((![X44]:(![X45]:(((~happens(X44,X45)|~less(X41,X45))|~less(X45,X42))|~initiates(X44,X43,X45))))|startedIn(X41,X43,X42)))))),inference(skolemize,[status(esa)],[c53])).])).
% 0.41/0.58 fof(c56,plain,(![X36]:(![X37]:(![X38]:(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:(((((~startedIn(X36,X38,X37)|happens(skolem0005(X36,X37,X38),skolem0006(X36,X37,X38)))&(~startedIn(X36,X38,X37)|less(X36,skolem0006(X36,X37,X38))))&(~startedIn(X36,X38,X37)|less(skolem0006(X36,X37,X38),X37)))&(~startedIn(X36,X38,X37)|initiates(skolem0005(X36,X37,X38),X38,skolem0006(X36,X37,X38))))&((((~happens(X44,X45)|~less(X41,X45))|~less(X45,X42))|~initiates(X44,X43,X45))|startedIn(X41,X43,X42))))))))))),inference(distribute,[status(thm)],[c55])).
% 0.41/0.58 cnf(c61,plain,~happens(X101,X105)|~less(X104,X105)|~less(X105,X102)|~initiates(X101,X103,X105)|startedIn(X104,X103,X102),inference(split_conjunct,[status(thm)],[c56])).
% 0.41/0.58 fof(keep_not_released,axiom,(![Fluent]:(![Time]:(((~releasedAt(Fluent,Time))&(~(?[Event]:(happens(Event,Time)&releases(Event,Fluent,Time)))))=>(~releasedAt(Fluent,plus(Time,n1)))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', keep_not_released)).
% 0.41/0.58 fof(c16,plain,(![Fluent]:(![Time]:((~releasedAt(Fluent,Time)&(~(?[Event]:(happens(Event,Time)&releases(Event,Fluent,Time)))))=>~releasedAt(Fluent,plus(Time,n1))))),inference(fof_simplification,[status(thm)],[keep_not_released])).
% 0.41/0.58 fof(c17,plain,(![Fluent]:(![Time]:((releasedAt(Fluent,Time)|(?[Event]:(happens(Event,Time)&releases(Event,Fluent,Time))))|~releasedAt(Fluent,plus(Time,n1))))),inference(fof_nnf,[status(thm)],[c16])).
% 0.41/0.58 fof(c18,plain,(![X14]:(![X15]:((releasedAt(X14,X15)|(?[X16]:(happens(X16,X15)&releases(X16,X14,X15))))|~releasedAt(X14,plus(X15,n1))))),inference(variable_rename,[status(thm)],[c17])).
% 0.41/0.58 fof(c19,plain,(![X14]:(![X15]:((releasedAt(X14,X15)|(happens(skolem0001(X14,X15),X15)&releases(skolem0001(X14,X15),X14,X15)))|~releasedAt(X14,plus(X15,n1))))),inference(skolemize,[status(esa)],[c18])).
% 0.41/0.58 fof(c20,plain,(![X14]:(![X15]:(((releasedAt(X14,X15)|happens(skolem0001(X14,X15),X15))|~releasedAt(X14,plus(X15,n1)))&((releasedAt(X14,X15)|releases(skolem0001(X14,X15),X14,X15))|~releasedAt(X14,plus(X15,n1)))))),inference(distribute,[status(thm)],[c19])).
% 0.41/0.58 cnf(c22,plain,releasedAt(X100,X99)|releases(skolem0001(X100,X99),X100,X99)|~releasedAt(X100,plus(X99,n1)),inference(split_conjunct,[status(thm)],[c20])).
% 0.41/0.58 cnf(c27,plain,~releasedAt(X98,X97)|happens(skolem0002(X98,X97),X97)|releasedAt(X98,plus(X97,n1)),inference(split_conjunct,[status(thm)],[c26])).
% 0.41/0.58 cnf(c71,plain,~stoppedIn(X96,X95,X94)|terminates(skolem0007(X96,X95,X94),X95,skolem0008(X96,X95,X94)),inference(split_conjunct,[status(thm)],[c67])).
% 0.41/0.58 cnf(c60,plain,~startedIn(X91,X92,X93)|initiates(skolem0005(X91,X93,X92),X92,skolem0006(X91,X93,X92)),inference(split_conjunct,[status(thm)],[c56])).
% 0.41/0.58 cnf(c21,plain,releasedAt(X90,X89)|happens(skolem0001(X90,X89),X89)|~releasedAt(X90,plus(X89,n1)),inference(split_conjunct,[status(thm)],[c20])).
% 0.41/0.59 cnf(c68,plain,~stoppedIn(X88,X87,X86)|happens(skolem0007(X88,X87,X86),skolem0008(X88,X87,X86)),inference(split_conjunct,[status(thm)],[c67])).
% 0.41/0.59 cnf(c57,plain,~startedIn(X83,X84,X85)|happens(skolem0005(X83,X85,X84),skolem0006(X83,X85,X84)),inference(split_conjunct,[status(thm)],[c56])).
% 0.41/0.59 fof(happens_holds,axiom,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&initiates(Event,Fluent,Time))=>holdsAt(Fluent,plus(Time,n1)))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', happens_holds)).
% 0.41/0.59 fof(c13,plain,(![Event]:(![Time]:(![Fluent]:((~happens(Event,Time)|~initiates(Event,Fluent,Time))|holdsAt(Fluent,plus(Time,n1)))))),inference(fof_nnf,[status(thm)],[happens_holds])).
% 0.41/0.59 fof(c14,plain,(![X11]:(![X12]:(![X13]:((~happens(X11,X12)|~initiates(X11,X13,X12))|holdsAt(X13,plus(X12,n1)))))),inference(variable_rename,[status(thm)],[c13])).
% 0.41/0.59 cnf(c15,plain,~happens(X80,X81)|~initiates(X80,X82,X81)|holdsAt(X82,plus(X81,n1)),inference(split_conjunct,[status(thm)],[c14])).
% 0.41/0.59 fof(happens_terminates_not_holds,axiom,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&terminates(Event,Fluent,Time))=>(~holdsAt(Fluent,plus(Time,n1))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', happens_terminates_not_holds)).
% 0.41/0.59 fof(c9,plain,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&terminates(Event,Fluent,Time))=>~holdsAt(Fluent,plus(Time,n1)))))),inference(fof_simplification,[status(thm)],[happens_terminates_not_holds])).
% 0.41/0.59 fof(c10,plain,(![Event]:(![Time]:(![Fluent]:((~happens(Event,Time)|~terminates(Event,Fluent,Time))|~holdsAt(Fluent,plus(Time,n1)))))),inference(fof_nnf,[status(thm)],[c9])).
% 0.41/0.59 fof(c11,plain,(![X8]:(![X9]:(![X10]:((~happens(X8,X9)|~terminates(X8,X10,X9))|~holdsAt(X10,plus(X9,n1)))))),inference(variable_rename,[status(thm)],[c10])).
% 0.41/0.59 cnf(c12,plain,~happens(X78,X77)|~terminates(X78,X79,X77)|~holdsAt(X79,plus(X77,n1)),inference(split_conjunct,[status(thm)],[c11])).
% 0.41/0.59 fof(happens_releases,axiom,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&releases(Event,Fluent,Time))=>releasedAt(Fluent,plus(Time,n1)))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', happens_releases)).
% 0.41/0.59 fof(c6,plain,(![Event]:(![Time]:(![Fluent]:((~happens(Event,Time)|~releases(Event,Fluent,Time))|releasedAt(Fluent,plus(Time,n1)))))),inference(fof_nnf,[status(thm)],[happens_releases])).
% 0.41/0.59 fof(c7,plain,(![X5]:(![X6]:(![X7]:((~happens(X5,X6)|~releases(X5,X7,X6))|releasedAt(X7,plus(X6,n1)))))),inference(variable_rename,[status(thm)],[c6])).
% 0.41/0.59 cnf(c8,plain,~happens(X76,X74)|~releases(X76,X75,X74)|releasedAt(X75,plus(X74,n1)),inference(split_conjunct,[status(thm)],[c7])).
% 0.41/0.59 fof(happens_not_released,axiom,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&(initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time)))=>(~releasedAt(Fluent,plus(Time,n1))))))),file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax', happens_not_released)).
% 0.41/0.59 fof(c0,plain,(![Event]:(![Time]:(![Fluent]:((happens(Event,Time)&(initiates(Event,Fluent,Time)|terminates(Event,Fluent,Time)))=>~releasedAt(Fluent,plus(Time,n1)))))),inference(fof_simplification,[status(thm)],[happens_not_released])).
% 0.41/0.59 fof(c1,plain,(![Event]:(![Time]:(![Fluent]:((~happens(Event,Time)|(~initiates(Event,Fluent,Time)&~terminates(Event,Fluent,Time)))|~releasedAt(Fluent,plus(Time,n1)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.41/0.59 fof(c2,plain,(![X2]:(![X3]:(![X4]:((~happens(X2,X3)|(~initiates(X2,X4,X3)&~terminates(X2,X4,X3)))|~releasedAt(X4,plus(X3,n1)))))),inference(variable_rename,[status(thm)],[c1])).
% 0.41/0.59 fof(c3,plain,(![X2]:(![X3]:(![X4]:(((~happens(X2,X3)|~initiates(X2,X4,X3))|~releasedAt(X4,plus(X3,n1)))&((~happens(X2,X3)|~terminates(X2,X4,X3))|~releasedAt(X4,plus(X3,n1))))))),inference(distribute,[status(thm)],[c2])).
% 0.41/0.59 cnf(c5,plain,~happens(X71,X73)|~terminates(X71,X72,X73)|~releasedAt(X72,plus(X73,n1)),inference(split_conjunct,[status(thm)],[c3])).
% 0.41/0.59 cnf(c4,plain,~happens(X68,X70)|~initiates(X68,X69,X70)|~releasedAt(X69,plus(X70,n1)),inference(split_conjunct,[status(thm)],[c3])).
% 0.41/0.59 cnf(c70,plain,~stoppedIn(X67,X66,X65)|less(skolem0008(X67,X66,X65),X65),inference(split_conjunct,[status(thm)],[c67])).
% 0.41/0.59 cnf(c69,plain,~stoppedIn(X64,X63,X62)|less(X64,skolem0008(X64,X63,X62)),inference(split_conjunct,[status(thm)],[c67])).
% 0.41/0.59 cnf(c59,plain,~startedIn(X59,X60,X61)|less(skolem0006(X59,X61,X60),X61),inference(split_conjunct,[status(thm)],[c56])).
% 0.41/0.59 cnf(c58,plain,~startedIn(X56,X57,X58)|less(X56,skolem0006(X56,X58,X57)),inference(split_conjunct,[status(thm)],[c56])).
% 0.41/0.59 % SZS output end Saturation
% 0.41/0.59
% 0.41/0.59 % Initial clauses : 25
% 0.41/0.59 % Processed clauses : 25
% 0.41/0.59 % Factors computed : 0
% 0.41/0.59 % Resolvents computed: 0
% 0.41/0.59 % Tautologies deleted: 0
% 0.41/0.59 % Forward subsumed : 0
% 0.41/0.59 % Backward subsumed : 0
% 0.41/0.59 % -------- CPU Time ---------
% 0.41/0.59 % User time : 0.214 s
% 0.41/0.59 % System time : 0.013 s
% 0.41/0.59 % Total time : 0.227 s
%------------------------------------------------------------------------------