%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ162_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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 : Tue May 5 06:49:04 PM UTC 2026 % Result : Theorem 5.04s 5.28s % Output : Proof 5.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ162_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.15/0.34 % Computer : n009.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 05:02:26 EDT 2026 % 0.15/0.34 % CPUTime : % 5.04/5.28 SZS status Theorem for theBenchmark.p % 5.04/5.28 SZS output start Proof for theBenchmark.p % 5.04/5.28 Clause #3 (by assumption #[]): Eq (∀ (E : event), armistice E → contentiousEvent E) True % 5.04/5.28 Clause #4 (by assumption #[]): Eq (∀ (E : event), armistice E → diplomaticEvent E) True % 5.04/5.28 Clause #5 (by assumption #[]): Eq (∀ (X Y Z : geographicalRegion), And (subRegions X Y) (subRegions Y Z) → subRegions X Z) True % 5.04/5.28 Clause #6 (by assumption #[]): Eq (∀ (X Y : geographicalRegion) (Z : event), And (eventOccursAt Z X) (subRegions Y X) → eventOccursAt Z Y) True % 5.04/5.28 Clause #7 (by assumption #[]): Eq (subRegions picardy rethondesCompiegne) True % 5.04/5.28 Clause #8 (by assumption #[]): Eq (subRegions hautsDeFrance picardy) True % 5.04/5.28 Clause #9 (by assumption #[]): Eq (subRegions france hautsDeFrance) True % 5.04/5.28 Clause #10 (by assumption #[]): Eq % 5.04/5.28 (∀ (CC : constrCont) (PR LT BW : govt), % 5.04/5.28 And (narrativeSuccessor CC PR BW) (narrativeSuccessor CC BW LT) → narrativeSuccessor CC PR LT) % 5.04/5.28 True % 5.04/5.28 Clause #16 (by assumption #[]): Eq (narrativeSuccessor marianne thirdRepublicFrench fourthRepublicFrench) True % 5.04/5.28 Clause #17 (by assumption #[]): Eq (narrativeSuccessor marianne fourthRepublicFrench fifthRepublicFrench) True % 5.04/5.28 Clause #32 (by assumption #[]): Eq (armistice armistice1940) True % 5.04/5.28 Clause #33 (by assumption #[]): Eq (eventOccursAt armistice1940 rethondesCompiegne) True % 5.04/5.28 Clause #34 (by assumption #[]): Eq (govtRepresentedBy armistice1940 thirdRepublicFrench hutzinger) True % 5.04/5.28 Clause #42 (by assumption #[]): Eq (seatingEvent armistice1940FrenchSeating) True % 5.04/5.28 Clause #43 (by assumption #[]): Eq (subEvents armistice1940 armistice1940FrenchSeating) True % 5.04/5.28 Clause #44 (by assumption #[]): Eq (performedBy armistice1940FrenchSeating hutzinger) True % 5.04/5.28 Clause #45 (by assumption #[]): Eq (seatedAtSide armistice1940FrenchSeating cwlTableSideC) True % 5.04/5.28 Clause #47 (by assumption #[]): Eq (eventOccursAt compiegneVisit2018 rethondesCompiegne) True % 5.04/5.28 Clause #49 (by assumption #[]): Eq (friendlyEvent compiegneVisit2018) True % 5.04/5.28 Clause #51 (by assumption #[]): Eq (govtRepresentedBy compiegneVisit2018 fifthRepublicFrench macron) True % 5.04/5.28 Clause #52 (by assumption #[]): Eq (endsBeforeStartOf armistice1940 compiegneVisit2018) True % 5.04/5.28 Clause #53 (by assumption #[]): Eq % 5.04/5.28 (∀ (DE VE : event) (LOC : geographicalRegion), % 5.04/5.28 And (And (And (diplomaticEvent DE) (eventOccursAt DE LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf DE VE) → % 5.04/5.28 pastColocatedDiplomaticEvent VE DE) % 5.04/5.28 True % 5.04/5.28 Clause #54 (by assumption #[]): Eq % 5.04/5.28 (∀ (P RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.04/5.28 And % 5.04/5.28 (And % 5.04/5.28 (And % 5.04/5.28 (And % 5.04/5.28 (And % 5.04/5.28 (And % 5.04/5.28 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.04/5.28 (seatingEvent SE)) % 5.04/5.28 (performedBy SE RP)) % 5.04/5.28 (seatedAtSide SE TS)) % 5.04/5.28 (govtRepresentedBy DE PASTGOVT RP)) % 5.04/5.28 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.04/5.28 (friendlyEvent VE)) % 5.04/5.28 (govtRepresentedBy VE GOVT P) → % 5.04/5.28 avoidTableSide P VE TS) % 5.04/5.28 True % 5.04/5.28 Clause #55 (by assumption #[]): Eq (Not (avoidTableSide macron compiegneVisit2018 cwlTableSideC)) True % 5.04/5.28 Clause #68 (by clausification #[3]): ∀ (a : event), Eq (armistice a → contentiousEvent a) True % 5.04/5.28 Clause #69 (by clausification #[68]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (contentiousEvent a) True) % 5.04/5.28 Clause #70 (by superposition #[69, 32]): Or (Eq (contentiousEvent armistice1940) True) (Eq False True) % 5.04/5.28 Clause #72 (by clausification #[4]): ∀ (a : event), Eq (armistice a → diplomaticEvent a) True % 5.04/5.28 Clause #73 (by clausification #[72]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (diplomaticEvent a) True) % 5.04/5.28 Clause #74 (by superposition #[73, 32]): Or (Eq (diplomaticEvent armistice1940) True) (Eq False True) % 5.04/5.28 Clause #77 (by clausification #[5]): ∀ (a : geographicalRegion), % 5.04/5.28 Eq (∀ (Y Z : geographicalRegion), And (subRegions a Y) (subRegions Y Z) → subRegions a Z) True % 5.04/5.28 Clause #78 (by clausification #[77]): ∀ (a a_1 : geographicalRegion), % 5.04/5.28 Eq (∀ (Z : geographicalRegion), And (subRegions a a_1) (subRegions a_1 Z) → subRegions a Z) True % 5.04/5.29 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : geographicalRegion), Eq (And (subRegions a a_1) (subRegions a_1 a_2) → subRegions a a_2) True % 5.04/5.29 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : geographicalRegion), % 5.04/5.29 Or (Eq (And (subRegions a a_1) (subRegions a_1 a_2)) False) (Eq (subRegions a a_2) True) % 5.04/5.29 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : geographicalRegion), % 5.04/5.29 Or (Eq (subRegions a a_1) True) (Or (Eq (subRegions a a_2) False) (Eq (subRegions a_2 a_1) False)) % 5.04/5.29 Clause #82 (by superposition #[81, 9]): ∀ (a : geographicalRegion), % 5.04/5.29 Or (Eq (subRegions france a) True) (Or (Eq (subRegions hautsDeFrance a) False) (Eq False True)) % 5.04/5.29 Clause #83 (by superposition #[81, 8]): ∀ (a : geographicalRegion), % 5.04/5.29 Or (Eq (subRegions hautsDeFrance a) True) (Or (Eq (subRegions picardy a) False) (Eq False True)) % 5.04/5.29 Clause #86 (by clausification #[6]): ∀ (a : geographicalRegion), % 5.04/5.29 Eq (∀ (Y : geographicalRegion) (Z : event), And (eventOccursAt Z a) (subRegions Y a) → eventOccursAt Z Y) True % 5.04/5.29 Clause #87 (by clausification #[86]): ∀ (a a_1 : geographicalRegion), % 5.04/5.29 Eq (∀ (Z : event), And (eventOccursAt Z a) (subRegions a_1 a) → eventOccursAt Z a_1) True % 5.04/5.29 Clause #88 (by clausification #[87]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.04/5.29 Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1) → eventOccursAt a a_2) True % 5.04/5.29 Clause #89 (by clausification #[88]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.04/5.29 Or (Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1)) False) (Eq (eventOccursAt a a_2) True) % 5.04/5.29 Clause #90 (by clausification #[89]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.04/5.29 Or (Eq (eventOccursAt a a_1) True) (Or (Eq (eventOccursAt a a_2) False) (Eq (subRegions a_1 a_2) False)) % 5.04/5.29 Clause #91 (by superposition #[90, 33]): ∀ (a : geographicalRegion), % 5.04/5.29 Or (Eq (eventOccursAt armistice1940 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 5.04/5.29 Clause #93 (by superposition #[90, 47]): ∀ (a : geographicalRegion), % 5.04/5.30 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 5.04/5.30 Clause #94 (by clausification #[10]): ∀ (a : constrCont), % 5.04/5.30 Eq (∀ (PR LT BW : govt), And (narrativeSuccessor a PR BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a PR LT) % 5.04/5.30 True % 5.04/5.30 Clause #95 (by clausification #[94]): ∀ (a : constrCont) (a_1 : govt), % 5.04/5.30 Eq (∀ (LT BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a a_1 LT) % 5.04/5.30 True % 5.04/5.30 Clause #96 (by clausification #[95]): ∀ (a : constrCont) (a_1 a_2 : govt), % 5.04/5.30 Eq (∀ (BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW a_2) → narrativeSuccessor a a_1 a_2) % 5.04/5.30 True % 5.04/5.30 Clause #97 (by clausification #[96]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.04/5.30 Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3) → narrativeSuccessor a a_1 a_3) True % 5.04/5.30 Clause #98 (by clausification #[97]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.04/5.30 Or (Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3)) False) % 5.04/5.30 (Eq (narrativeSuccessor a a_1 a_3) True) % 5.04/5.30 Clause #99 (by clausification #[98]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.04/5.30 Or (Eq (narrativeSuccessor a a_1 a_2) True) % 5.04/5.30 (Or (Eq (narrativeSuccessor a a_1 a_3) False) (Eq (narrativeSuccessor a a_3 a_2) False)) % 5.04/5.30 Clause #105 (by clausification #[74]): Eq (diplomaticEvent armistice1940) True % 5.04/5.30 Clause #108 (by clausification #[70]): Eq (contentiousEvent armistice1940) True % 5.04/5.30 Clause #109 (by superposition #[16, 99]): ∀ (a : govt), % 5.04/5.30 Or (Eq (narrativeSuccessor marianne thirdRepublicFrench a) True) % 5.04/5.30 (Or (Eq (narrativeSuccessor marianne fourthRepublicFrench a) False) (Eq False True)) % 5.04/5.30 Clause #112 (by clausification #[55]): Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) False % 5.04/5.30 Clause #113 (by clausification #[53]): ∀ (a : event), % 5.04/5.30 Eq % 5.04/5.30 (∀ (VE : event) (LOC : geographicalRegion), % 5.04/5.30 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf a VE) → % 5.14/5.31 pastColocatedDiplomaticEvent VE a) % 5.14/5.31 True % 5.14/5.31 Clause #114 (by clausification #[113]): ∀ (a a_1 : event), % 5.14/5.31 Eq % 5.14/5.31 (∀ (LOC : geographicalRegion), % 5.14/5.31 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt a_1 LOC)) (endsBeforeStartOf a a_1) → % 5.14/5.31 pastColocatedDiplomaticEvent a_1 a) % 5.14/5.31 True % 5.14/5.31 Clause #115 (by clausification #[114]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 5.14/5.31 Eq % 5.14/5.31 (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2) → % 5.14/5.31 pastColocatedDiplomaticEvent a_2 a) % 5.14/5.31 True % 5.14/5.31 Clause #116 (by clausification #[115]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 5.14/5.31 Or % 5.14/5.31 (Eq (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2)) % 5.14/5.31 False) % 5.14/5.31 (Eq (pastColocatedDiplomaticEvent a_2 a) True) % 5.14/5.31 Clause #117 (by clausification #[116]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.14/5.31 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.14/5.31 (Or (Eq (And (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) (eventOccursAt a a_2)) False) % 5.14/5.31 (Eq (endsBeforeStartOf a_1 a) False)) % 5.14/5.31 Clause #118 (by clausification #[117]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.14/5.31 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.14/5.31 (Or (Eq (endsBeforeStartOf a_1 a) False) % 5.14/5.31 (Or (Eq (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) False) (Eq (eventOccursAt a a_2) False))) % 5.14/5.31 Clause #119 (by clausification #[118]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.14/5.31 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.14/5.31 (Or (Eq (endsBeforeStartOf a_1 a) False) % 5.14/5.31 (Or (Eq (eventOccursAt a a_2) False) (Or (Eq (diplomaticEvent a_1) False) (Eq (eventOccursAt a_1 a_2) False)))) % 5.14/5.31 Clause #120 (by superposition #[119, 52]): ∀ (a : geographicalRegion), % 5.14/5.31 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.31 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 5.14/5.31 (Or (Eq (diplomaticEvent armistice1940) False) (Or (Eq (eventOccursAt armistice1940 a) False) (Eq False True)))) % 5.14/5.31 Clause #122 (by clausification #[93]): ∀ (a : geographicalRegion), % 5.14/5.31 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a rethondesCompiegne) False) % 5.14/5.31 Clause #123 (by superposition #[122, 7]): Or (Eq (eventOccursAt compiegneVisit2018 picardy) True) (Eq False True) % 5.14/5.31 Clause #124 (by clausification #[123]): Eq (eventOccursAt compiegneVisit2018 picardy) True % 5.14/5.31 Clause #125 (by superposition #[124, 90]): ∀ (a : geographicalRegion), % 5.14/5.31 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a picardy) False)) % 5.14/5.31 Clause #126 (by clausification #[125]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a picardy) False) % 5.14/5.31 Clause #127 (by superposition #[126, 8]): Or (Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True) (Eq False True) % 5.14/5.31 Clause #128 (by clausification #[127]): Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True % 5.14/5.31 Clause #129 (by superposition #[128, 90]): ∀ (a : geographicalRegion), % 5.14/5.31 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a hautsDeFrance) False)) % 5.14/5.31 Clause #130 (by clausification #[129]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a hautsDeFrance) False) % 5.14/5.31 Clause #131 (by superposition #[130, 9]): Or (Eq (eventOccursAt compiegneVisit2018 france) True) (Eq False True) % 5.14/5.31 Clause #132 (by clausification #[54]): ∀ (a : person), % 5.14/5.31 Eq % 5.14/5.31 (∀ (RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.14/5.31 And % 5.14/5.31 (And % 5.14/5.31 (And % 5.14/5.31 (And % 5.14/5.31 (And % 5.14/5.31 (And % 5.14/5.31 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.31 (seatingEvent SE)) % 5.14/5.31 (performedBy SE RP)) % 5.14/5.31 (seatedAtSide SE TS)) % 5.14/5.31 (govtRepresentedBy DE PASTGOVT RP)) % 5.14/5.31 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.14/5.31 (friendlyEvent VE)) % 5.14/5.33 (govtRepresentedBy VE GOVT a) → % 5.14/5.33 avoidTableSide a VE TS) % 5.14/5.33 True % 5.14/5.33 Clause #133 (by clausification #[132]): ∀ (a a_1 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.33 (seatingEvent SE)) % 5.14/5.33 (performedBy SE a)) % 5.14/5.33 (seatedAtSide SE TS)) % 5.14/5.33 (govtRepresentedBy DE PASTGOVT a)) % 5.14/5.33 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.14/5.33 (friendlyEvent VE)) % 5.14/5.33 (govtRepresentedBy VE GOVT a_1) → % 5.14/5.33 avoidTableSide a_1 VE TS) % 5.14/5.33 True % 5.14/5.33 Clause #134 (by clausification #[133]): ∀ (a : person) (a_1 : govt) (a_2 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.33 (seatingEvent SE)) % 5.14/5.33 (performedBy SE a)) % 5.14/5.33 (seatedAtSide SE TS)) % 5.14/5.33 (govtRepresentedBy DE a_1 a)) % 5.14/5.33 (narrativeSuccessor CC a_1 GOVT)) % 5.14/5.33 (friendlyEvent VE)) % 5.14/5.33 (govtRepresentedBy VE GOVT a_2) → % 5.14/5.33 avoidTableSide a_2 VE TS) % 5.14/5.33 True % 5.14/5.33 Clause #135 (by clausification #[134]): ∀ (a : person) (a_1 a_2 : govt) (a_3 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.33 (seatingEvent SE)) % 5.14/5.33 (performedBy SE a)) % 5.14/5.33 (seatedAtSide SE TS)) % 5.14/5.33 (govtRepresentedBy DE a_1 a)) % 5.14/5.33 (narrativeSuccessor CC a_1 a_2)) % 5.14/5.33 (friendlyEvent VE)) % 5.14/5.33 (govtRepresentedBy VE a_2 a_3) → % 5.14/5.33 avoidTableSide a_3 VE TS) % 5.14/5.33 True % 5.14/5.33 Clause #136 (by clausification #[135]): ∀ (a : person) (a_1 : govt) (a_2 : constrCont) (a_3 : govt) (a_4 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (VE DE SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.33 (seatingEvent SE)) % 5.14/5.33 (performedBy SE a)) % 5.14/5.33 (seatedAtSide SE TS)) % 5.14/5.33 (govtRepresentedBy DE a_1 a)) % 5.14/5.33 (narrativeSuccessor a_2 a_1 a_3)) % 5.14/5.33 (friendlyEvent VE)) % 5.14/5.33 (govtRepresentedBy VE a_3 a_4) → % 5.14/5.33 avoidTableSide a_4 VE TS) % 5.14/5.33 True % 5.14/5.33 Clause #137 (by clausification #[136]): ∀ (a : event) (a_1 : person) (a_2 : govt) (a_3 : constrCont) (a_4 : govt) (a_5 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (DE SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent a DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.14/5.33 (seatingEvent SE)) % 5.14/5.33 (performedBy SE a_1)) % 5.14/5.33 (seatedAtSide SE TS)) % 5.14/5.33 (govtRepresentedBy DE a_2 a_1)) % 5.14/5.33 (narrativeSuccessor a_3 a_2 a_4)) % 5.14/5.33 (friendlyEvent a)) % 5.14/5.33 (govtRepresentedBy a a_4 a_5) → % 5.14/5.33 avoidTableSide a_5 a TS) % 5.14/5.33 True % 5.14/5.33 Clause #138 (by clausification #[137]): ∀ (a a_1 : event) (a_2 : person) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : person), % 5.14/5.33 Eq % 5.14/5.33 (∀ (SE : event) (TS : table_side), % 5.14/5.33 And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And % 5.14/5.33 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 SE)) % 5.14/5.34 (seatingEvent SE)) % 5.14/5.34 (performedBy SE a_2)) % 5.14/5.34 (seatedAtSide SE TS)) % 5.14/5.34 (govtRepresentedBy a_1 a_3 a_2)) % 5.14/5.34 (narrativeSuccessor a_4 a_3 a_5)) % 5.14/5.34 (friendlyEvent a)) % 5.14/5.34 (govtRepresentedBy a a_5 a_6) → % 5.14/5.34 avoidTableSide a_6 a TS) % 5.14/5.34 True % 5.14/5.34 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : govt) (a_5 : constrCont) (a_6 : govt) (a_7 : person), % 5.14/5.34 Eq % 5.14/5.34 (∀ (TS : table_side), % 5.14/5.34 And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.14/5.34 (seatingEvent a_2)) % 5.14/5.34 (performedBy a_2 a_3)) % 5.14/5.34 (seatedAtSide a_2 TS)) % 5.14/5.34 (govtRepresentedBy a_1 a_4 a_3)) % 5.14/5.34 (narrativeSuccessor a_5 a_4 a_6)) % 5.14/5.34 (friendlyEvent a)) % 5.14/5.34 (govtRepresentedBy a a_6 a_7) → % 5.14/5.34 avoidTableSide a_7 a TS) % 5.14/5.34 True % 5.14/5.34 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : table_side) (a_5 : govt) (a_6 : constrCont) (a_7 : govt) (a_8 : person), % 5.14/5.34 Eq % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.14/5.34 (seatingEvent a_2)) % 5.14/5.34 (performedBy a_2 a_3)) % 5.14/5.34 (seatedAtSide a_2 a_4)) % 5.14/5.34 (govtRepresentedBy a_1 a_5 a_3)) % 5.14/5.34 (narrativeSuccessor a_6 a_5 a_7)) % 5.14/5.34 (friendlyEvent a)) % 5.14/5.34 (govtRepresentedBy a a_7 a_8) → % 5.14/5.34 avoidTableSide a_8 a a_4) % 5.14/5.34 True % 5.14/5.34 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : event) (a_3 : person) (a_4 : table_side) (a_5 : govt) (a_6 : constrCont) (a_7 : govt) (a_8 : person), % 5.14/5.34 Or % 5.14/5.34 (Eq % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.14/5.34 (seatingEvent a_2)) % 5.14/5.34 (performedBy a_2 a_3)) % 5.14/5.34 (seatedAtSide a_2 a_4)) % 5.14/5.34 (govtRepresentedBy a_1 a_5 a_3)) % 5.14/5.34 (narrativeSuccessor a_6 a_5 a_7)) % 5.14/5.34 (friendlyEvent a)) % 5.14/5.34 (govtRepresentedBy a a_7 a_8)) % 5.14/5.34 False) % 5.14/5.34 (Eq (avoidTableSide a_8 a a_4) True) % 5.14/5.34 Clause #142 (by clausification #[141]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 a_4 : event) (a_5 : person) (a_6 : govt) (a_7 : constrCont) % 5.14/5.34 (a_8 : govt), % 5.14/5.34 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.34 (Or % 5.14/5.34 (Eq % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And (And (And (pastColocatedDiplomaticEvent a_1 a_3) (contentiousEvent a_3)) (subEvents a_3 a_4)) % 5.14/5.34 (seatingEvent a_4)) % 5.14/5.34 (performedBy a_4 a_5)) % 5.14/5.34 (seatedAtSide a_4 a_2)) % 5.14/5.34 (govtRepresentedBy a_3 a_6 a_5)) % 5.14/5.34 (narrativeSuccessor a_7 a_6 a_8)) % 5.14/5.34 (friendlyEvent a_1)) % 5.14/5.34 False) % 5.14/5.34 (Eq (govtRepresentedBy a_1 a_8 a) False)) % 5.14/5.34 Clause #143 (by clausification #[142]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 a_5 : event) (a_6 : person) (a_7 : govt) % 5.14/5.34 (a_8 : constrCont), % 5.14/5.34 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.34 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.34 (Or % 5.14/5.34 (Eq % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And % 5.14/5.34 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 5.14/5.34 (seatingEvent a_5)) % 5.14/5.34 (performedBy a_5 a_6)) % 5.14/5.34 (seatedAtSide a_5 a_2)) % 5.14/5.34 (govtRepresentedBy a_4 a_7 a_6)) % 5.14/5.34 (narrativeSuccessor a_8 a_7 a_3)) % 5.14/5.34 False) % 5.14/5.34 (Eq (friendlyEvent a_1) False))) % 5.14/5.34 Clause #144 (by clausification #[143]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 a_5 : event) (a_6 : person) (a_7 : govt) % 5.14/5.36 (a_8 : constrCont), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or % 5.14/5.36 (Eq % 5.14/5.36 (And % 5.14/5.36 (And % 5.14/5.36 (And % 5.14/5.36 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 5.14/5.36 (seatingEvent a_5)) % 5.14/5.36 (performedBy a_5 a_6)) % 5.14/5.36 (seatedAtSide a_5 a_2)) % 5.14/5.36 (govtRepresentedBy a_4 a_7 a_6)) % 5.14/5.36 False) % 5.14/5.36 (Eq (narrativeSuccessor a_8 a_7 a_3) False)))) % 5.14/5.36 Clause #145 (by clausification #[144]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 a_7 : event) % 5.14/5.36 (a_8 : person), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.36 (Or % 5.14/5.36 (Eq % 5.14/5.36 (And % 5.14/5.36 (And % 5.14/5.36 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_7)) % 5.14/5.36 (seatingEvent a_7)) % 5.14/5.36 (performedBy a_7 a_8)) % 5.14/5.36 (seatedAtSide a_7 a_2)) % 5.14/5.36 False) % 5.14/5.36 (Eq (govtRepresentedBy a_6 a_5 a_8) False))))) % 5.14/5.36 Clause #146 (by clausification #[145]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 5.14/5.36 (a_7 : person) (a_8 : event), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.14/5.36 (Or % 5.14/5.36 (Eq % 5.14/5.36 (And % 5.14/5.36 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.14/5.36 (seatingEvent a_8)) % 5.14/5.36 (performedBy a_8 a_7)) % 5.14/5.36 False) % 5.14/5.36 (Eq (seatedAtSide a_8 a_2) False)))))) % 5.14/5.36 Clause #147 (by clausification #[146]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 5.14/5.36 (a_7 : person) (a_8 : event), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.14/5.36 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.14/5.36 (Or % 5.14/5.36 (Eq % 5.14/5.36 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.14/5.36 (seatingEvent a_8)) % 5.14/5.36 False) % 5.14/5.36 (Eq (performedBy a_8 a_7) False))))))) % 5.14/5.36 Clause #148 (by clausification #[147]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 5.14/5.36 (a_7 : person) (a_8 : event), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.14/5.36 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.14/5.36 (Or (Eq (performedBy a_8 a_7) False) % 5.14/5.36 (Or % 5.14/5.36 (Eq (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.14/5.36 False) % 5.14/5.36 (Eq (seatingEvent a_8) False)))))))) % 5.14/5.36 Clause #149 (by clausification #[148]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 5.14/5.36 (a_7 : person) (a_8 : event), % 5.14/5.36 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.36 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.36 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.36 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.14/5.36 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.14/5.38 (Or (Eq (performedBy a_8 a_7) False) % 5.14/5.38 (Or (Eq (seatingEvent a_8) False) % 5.14/5.38 (Or (Eq (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) False) % 5.14/5.38 (Eq (subEvents a_6 a_8) False))))))))) % 5.14/5.38 Clause #150 (by clausification #[149]): ∀ (a : person) (a_1 : event) (a_2 : table_side) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : event) % 5.14/5.38 (a_7 : person) (a_8 : event), % 5.14/5.38 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.14/5.38 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.14/5.38 (Or (Eq (friendlyEvent a_1) False) % 5.14/5.38 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.14/5.38 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.14/5.38 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.14/5.38 (Or (Eq (performedBy a_8 a_7) False) % 5.14/5.38 (Or (Eq (seatingEvent a_8) False) % 5.14/5.38 (Or (Eq (subEvents a_6 a_8) False) % 5.14/5.38 (Or (Eq (pastColocatedDiplomaticEvent a_1 a_6) False) (Eq (contentiousEvent a_6) False)))))))))) % 5.14/5.38 Clause #155 (by superposition #[150, 51]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.14/5.38 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.38 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 5.14/5.38 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.14/5.38 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.14/5.38 (Or (Eq (seatedAtSide a_5 a) False) % 5.14/5.38 (Or (Eq (performedBy a_5 a_4) False) % 5.14/5.38 (Or (Eq (seatingEvent a_5) False) % 5.14/5.38 (Or (Eq (subEvents a_3 a_5) False) % 5.14/5.38 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.14/5.38 (Or (Eq (contentiousEvent a_3) False) (Eq False True)))))))))) % 5.14/5.38 Clause #157 (by clausification #[131]): Eq (eventOccursAt compiegneVisit2018 france) True % 5.14/5.38 Clause #167 (by clausification #[82]): ∀ (a : geographicalRegion), Or (Eq (subRegions france a) True) (Eq (subRegions hautsDeFrance a) False) % 5.14/5.38 Clause #173 (by clausification #[83]): ∀ (a : geographicalRegion), Or (Eq (subRegions hautsDeFrance a) True) (Eq (subRegions picardy a) False) % 5.14/5.38 Clause #174 (by superposition #[173, 7]): Or (Eq (subRegions hautsDeFrance rethondesCompiegne) True) (Eq False True) % 5.14/5.38 Clause #175 (by clausification #[91]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt armistice1940 a) True) (Eq (subRegions a rethondesCompiegne) False) % 5.14/5.38 Clause #179 (by clausification #[174]): Eq (subRegions hautsDeFrance rethondesCompiegne) True % 5.14/5.38 Clause #182 (by superposition #[179, 167]): Or (Eq (subRegions france rethondesCompiegne) True) (Eq True False) % 5.14/5.38 Clause #184 (by clausification #[182]): Eq (subRegions france rethondesCompiegne) True % 5.14/5.38 Clause #185 (by superposition #[184, 175]): Or (Eq (eventOccursAt armistice1940 france) True) (Eq True False) % 5.14/5.38 Clause #187 (by clausification #[185]): Eq (eventOccursAt armistice1940 france) True % 5.14/5.38 Clause #248 (by clausification #[109]): ∀ (a : govt), % 5.14/5.38 Or (Eq (narrativeSuccessor marianne thirdRepublicFrench a) True) % 5.14/5.38 (Eq (narrativeSuccessor marianne fourthRepublicFrench a) False) % 5.14/5.38 Clause #249 (by superposition #[248, 17]): Or (Eq (narrativeSuccessor marianne thirdRepublicFrench fifthRepublicFrench) True) (Eq False True) % 5.14/5.38 Clause #250 (by clausification #[249]): Eq (narrativeSuccessor marianne thirdRepublicFrench fifthRepublicFrench) True % 5.14/5.38 Clause #270 (by clausification #[120]): ∀ (a : geographicalRegion), % 5.14/5.38 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.38 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 5.14/5.38 (Or (Eq (diplomaticEvent armistice1940) False) (Eq (eventOccursAt armistice1940 a) False))) % 5.14/5.38 Clause #271 (by forward demodulation #[270, 105]): ∀ (a : geographicalRegion), % 5.14/5.38 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.38 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Or (Eq True False) (Eq (eventOccursAt armistice1940 a) False))) % 5.14/5.38 Clause #272 (by clausification #[271]): ∀ (a : geographicalRegion), % 5.14/5.38 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.39 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Eq (eventOccursAt armistice1940 a) False)) % 5.14/5.39 Clause #276 (by superposition #[272, 157]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.39 (Or (Eq (eventOccursAt armistice1940 france) False) (Eq False True)) % 5.14/5.39 Clause #277 (by clausification #[276]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) % 5.14/5.39 (Eq (eventOccursAt armistice1940 france) False) % 5.14/5.39 Clause #278 (by forward demodulation #[277, 187]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True) (Eq True False) % 5.14/5.39 Clause #279 (by clausification #[278]): Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) True % 5.14/5.39 Clause #369 (by clausification #[155]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 5.14/5.39 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.14/5.39 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.14/5.39 (Or (Eq (seatedAtSide a_5 a) False) % 5.14/5.39 (Or (Eq (performedBy a_5 a_4) False) % 5.14/5.39 (Or (Eq (seatingEvent a_5) False) % 5.14/5.39 (Or (Eq (subEvents a_3 a_5) False) % 5.14/5.39 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.14/5.39 (Eq (contentiousEvent a_3) False))))))))) % 5.14/5.39 Clause #370 (by forward demodulation #[369, 49]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq True False) % 5.14/5.39 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.14/5.39 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.14/5.39 (Or (Eq (seatedAtSide a_5 a) False) % 5.14/5.39 (Or (Eq (performedBy a_5 a_4) False) % 5.14/5.39 (Or (Eq (seatingEvent a_5) False) % 5.14/5.39 (Or (Eq (subEvents a_3 a_5) False) % 5.14/5.39 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.14/5.39 (Eq (contentiousEvent a_3) False))))))))) % 5.14/5.39 Clause #371 (by clausification #[370]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.14/5.39 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.14/5.39 (Or (Eq (seatedAtSide a_5 a) False) % 5.14/5.39 (Or (Eq (performedBy a_5 a_4) False) % 5.14/5.39 (Or (Eq (seatingEvent a_5) False) % 5.14/5.39 (Or (Eq (subEvents a_3 a_5) False) % 5.14/5.39 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.14/5.39 (Eq (contentiousEvent a_3) False)))))))) % 5.14/5.39 Clause #374 (by superposition #[371, 250]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq (govtRepresentedBy a_1 thirdRepublicFrench a_2) False) % 5.14/5.39 (Or (Eq (seatedAtSide a_3 a) False) % 5.14/5.39 (Or (Eq (performedBy a_3 a_2) False) % 5.14/5.39 (Or (Eq (seatingEvent a_3) False) % 5.14/5.39 (Or (Eq (subEvents a_1 a_3) False) % 5.14/5.39 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 5.14/5.39 (Or (Eq (contentiousEvent a_1) False) (Eq False True)))))))) % 5.14/5.39 Clause #375 (by clausification #[374]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq (govtRepresentedBy a_1 thirdRepublicFrench a_2) False) % 5.14/5.39 (Or (Eq (seatedAtSide a_3 a) False) % 5.14/5.39 (Or (Eq (performedBy a_3 a_2) False) % 5.14/5.39 (Or (Eq (seatingEvent a_3) False) % 5.14/5.39 (Or (Eq (subEvents a_1 a_3) False) % 5.14/5.39 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 5.14/5.39 (Eq (contentiousEvent a_1) False))))))) % 5.14/5.39 Clause #377 (by superposition #[375, 34]): ∀ (a : table_side) (a_1 : event), % 5.14/5.39 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.14/5.39 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) % 5.24/5.41 (Or (Eq (subEvents armistice1940 a_1) False) % 5.24/5.41 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) False) % 5.24/5.41 (Or (Eq (contentiousEvent armistice1940) False) (Eq False True))))))) % 5.24/5.41 Clause #378 (by clausification #[377]): ∀ (a : table_side) (a_1 : event), % 5.24/5.41 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.24/5.41 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) % 5.24/5.41 (Or (Eq (subEvents armistice1940 a_1) False) % 5.24/5.41 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1940) False) % 5.24/5.41 (Eq (contentiousEvent armistice1940) False)))))) % 5.24/5.41 Clause #379 (by forward demodulation #[378, 279]): ∀ (a : table_side) (a_1 : event), % 5.24/5.41 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.24/5.41 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) % 5.24/5.41 (Or (Eq (subEvents armistice1940 a_1) False) % 5.24/5.41 (Or (Eq True False) (Eq (contentiousEvent armistice1940) False)))))) % 5.24/5.41 Clause #380 (by clausification #[379]): ∀ (a : table_side) (a_1 : event), % 5.24/5.41 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.24/5.41 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) % 5.24/5.41 (Or (Eq (subEvents armistice1940 a_1) False) (Eq (contentiousEvent armistice1940) False))))) % 5.24/5.41 Clause #381 (by forward demodulation #[380, 108]): ∀ (a : table_side) (a_1 : event), % 5.24/5.41 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.24/5.41 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) (Or (Eq (subEvents armistice1940 a_1) False) (Eq True False))))) % 5.24/5.41 Clause #382 (by clausification #[381]): ∀ (a : table_side) (a_1 : event), % 5.24/5.41 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.24/5.41 (Or (Eq (seatedAtSide a_1 a) False) % 5.24/5.41 (Or (Eq (performedBy a_1 hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent a_1) False) (Eq (subEvents armistice1940 a_1) False)))) % 5.24/5.41 Clause #385 (by superposition #[382, 45]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Or (Eq (performedBy armistice1940FrenchSeating hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent armistice1940FrenchSeating) False) % 5.24/5.41 (Or (Eq (subEvents armistice1940 armistice1940FrenchSeating) False) (Eq False True)))) % 5.24/5.41 Clause #392 (by clausification #[385]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Or (Eq (performedBy armistice1940FrenchSeating hutzinger) False) % 5.24/5.41 (Or (Eq (seatingEvent armistice1940FrenchSeating) False) % 5.24/5.41 (Eq (subEvents armistice1940 armistice1940FrenchSeating) False))) % 5.24/5.41 Clause #393 (by forward demodulation #[392, 44]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Or (Eq True False) % 5.24/5.41 (Or (Eq (seatingEvent armistice1940FrenchSeating) False) % 5.24/5.41 (Eq (subEvents armistice1940 armistice1940FrenchSeating) False))) % 5.24/5.41 Clause #394 (by clausification #[393]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Or (Eq (seatingEvent armistice1940FrenchSeating) False) % 5.24/5.41 (Eq (subEvents armistice1940 armistice1940FrenchSeating) False)) % 5.24/5.41 Clause #395 (by forward demodulation #[394, 42]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Or (Eq True False) (Eq (subEvents armistice1940 armistice1940FrenchSeating) False)) % 5.24/5.41 Clause #396 (by clausification #[395]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) % 5.24/5.41 (Eq (subEvents armistice1940 armistice1940FrenchSeating) False) % 5.24/5.41 Clause #397 (by forward demodulation #[396, 43]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True) (Eq True False) % 5.24/5.41 Clause #398 (by clausification #[397]): Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideC) True % 5.24/5.41 Clause #399 (by superposition #[398, 112]): Eq True False % 5.24/5.41 Clause #401 (by clausification #[399]): False % 5.24/5.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------