%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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.44s 5.61s % Output : Proof 5.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PUZ161_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.16/0.33 % Computer : n019.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 05:01:44 EDT 2026 % 0.16/0.34 % CPUTime : % 5.44/5.61 SZS status Theorem for theBenchmark.p % 5.44/5.61 SZS output start Proof for theBenchmark.p % 5.44/5.61 Clause #0 (by assumption #[]): Eq (∀ (X Y Z : event), And (endsBeforeStartOf X Y) (endsBeforeStartOf Y Z) → endsBeforeStartOf X Z) True % 5.44/5.61 Clause #3 (by assumption #[]): Eq (∀ (E : event), armistice E → contentiousEvent E) True % 5.44/5.61 Clause #4 (by assumption #[]): Eq (∀ (E : event), armistice E → diplomaticEvent E) True % 5.44/5.61 Clause #5 (by assumption #[]): Eq (∀ (X Y Z : geographicalRegion), And (subRegions X Y) (subRegions Y Z) → subRegions X Z) True % 5.44/5.61 Clause #6 (by assumption #[]): Eq (∀ (X Y : geographicalRegion) (Z : event), And (eventOccursAt Z X) (subRegions Y X) → eventOccursAt Z Y) True % 5.44/5.61 Clause #7 (by assumption #[]): Eq (subRegions picardy rethondesCompiegne) True % 5.44/5.61 Clause #8 (by assumption #[]): Eq (subRegions hautsDeFrance picardy) True % 5.44/5.61 Clause #9 (by assumption #[]): Eq (subRegions france hautsDeFrance) True % 5.44/5.61 Clause #10 (by assumption #[]): Eq % 5.44/5.61 (∀ (CC : constrCont) (PR LT BW : govt), % 5.44/5.61 And (narrativeSuccessor CC PR BW) (narrativeSuccessor CC BW LT) → narrativeSuccessor CC PR LT) % 5.44/5.61 True % 5.44/5.61 Clause #16 (by assumption #[]): Eq (narrativeSuccessor marianne thirdRepublicFrench fourthRepublicFrench) True % 5.44/5.61 Clause #17 (by assumption #[]): Eq (narrativeSuccessor marianne fourthRepublicFrench fifthRepublicFrench) True % 5.44/5.61 Clause #18 (by assumption #[]): Eq (armistice armistice1918) True % 5.44/5.61 Clause #19 (by assumption #[]): Eq (eventOccursAt armistice1918 rethondesCompiegne) True % 5.44/5.61 Clause #20 (by assumption #[]): Eq (govtRepresentedBy armistice1918 thirdRepublicFrench foch) True % 5.44/5.61 Clause #22 (by assumption #[]): Eq (seatingEvent armistice1918AlliedSeating) True % 5.44/5.61 Clause #23 (by assumption #[]): Eq (subEvents armistice1918 armistice1918AlliedSeating) True % 5.44/5.61 Clause #24 (by assumption #[]): Eq (performedBy armistice1918AlliedSeating foch) True % 5.44/5.61 Clause #25 (by assumption #[]): Eq (seatedAtSide armistice1918AlliedSeating cwlTableSideA) True % 5.44/5.61 Clause #36 (by assumption #[]): Eq (endsBeforeStartOf armistice1918 armistice1940) True % 5.44/5.61 Clause #47 (by assumption #[]): Eq (eventOccursAt compiegneVisit2018 rethondesCompiegne) True % 5.44/5.61 Clause #49 (by assumption #[]): Eq (friendlyEvent compiegneVisit2018) True % 5.44/5.61 Clause #51 (by assumption #[]): Eq (govtRepresentedBy compiegneVisit2018 fifthRepublicFrench macron) True % 5.44/5.61 Clause #52 (by assumption #[]): Eq (endsBeforeStartOf armistice1940 compiegneVisit2018) True % 5.44/5.61 Clause #53 (by assumption #[]): Eq % 5.44/5.61 (∀ (DE VE : event) (LOC : geographicalRegion), % 5.44/5.61 And (And (And (diplomaticEvent DE) (eventOccursAt DE LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf DE VE) → % 5.44/5.61 pastColocatedDiplomaticEvent VE DE) % 5.44/5.61 True % 5.44/5.61 Clause #54 (by assumption #[]): Eq % 5.44/5.61 (∀ (P RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.44/5.61 And % 5.44/5.61 (And % 5.44/5.61 (And % 5.44/5.61 (And % 5.44/5.61 (And % 5.44/5.61 (And % 5.44/5.61 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.61 (seatingEvent SE)) % 5.44/5.61 (performedBy SE RP)) % 5.44/5.61 (seatedAtSide SE TS)) % 5.44/5.61 (govtRepresentedBy DE PASTGOVT RP)) % 5.44/5.61 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.44/5.61 (friendlyEvent VE)) % 5.44/5.61 (govtRepresentedBy VE GOVT P) → % 5.44/5.61 avoidTableSide P VE TS) % 5.44/5.61 True % 5.44/5.61 Clause #55 (by assumption #[]): Eq (Not (avoidTableSide macron compiegneVisit2018 cwlTableSideA)) True % 5.44/5.61 Clause #56 (by clausification #[0]): ∀ (a : event), Eq (∀ (Y Z : event), And (endsBeforeStartOf a Y) (endsBeforeStartOf Y Z) → endsBeforeStartOf a Z) True % 5.44/5.61 Clause #57 (by clausification #[56]): ∀ (a a_1 : event), % 5.44/5.61 Eq (∀ (Z : event), And (endsBeforeStartOf a a_1) (endsBeforeStartOf a_1 Z) → endsBeforeStartOf a Z) True % 5.44/5.61 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 : event), Eq (And (endsBeforeStartOf a a_1) (endsBeforeStartOf a_1 a_2) → endsBeforeStartOf a a_2) True % 5.44/5.61 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : event), % 5.44/5.61 Or (Eq (And (endsBeforeStartOf a a_1) (endsBeforeStartOf a_1 a_2)) False) (Eq (endsBeforeStartOf a a_2) True) % 5.44/5.61 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : event), % 5.44/5.63 Or (Eq (endsBeforeStartOf a a_1) True) % 5.44/5.63 (Or (Eq (endsBeforeStartOf a a_2) False) (Eq (endsBeforeStartOf a_2 a_1) False)) % 5.44/5.63 Clause #68 (by clausification #[3]): ∀ (a : event), Eq (armistice a → contentiousEvent a) True % 5.44/5.63 Clause #69 (by clausification #[68]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (contentiousEvent a) True) % 5.44/5.63 Clause #71 (by superposition #[69, 18]): Or (Eq (contentiousEvent armistice1918) True) (Eq False True) % 5.44/5.63 Clause #72 (by clausification #[4]): ∀ (a : event), Eq (armistice a → diplomaticEvent a) True % 5.44/5.63 Clause #73 (by clausification #[72]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (diplomaticEvent a) True) % 5.44/5.63 Clause #75 (by superposition #[73, 18]): Or (Eq (diplomaticEvent armistice1918) True) (Eq False True) % 5.44/5.63 Clause #77 (by clausification #[5]): ∀ (a : geographicalRegion), % 5.44/5.63 Eq (∀ (Y Z : geographicalRegion), And (subRegions a Y) (subRegions Y Z) → subRegions a Z) True % 5.44/5.63 Clause #78 (by clausification #[77]): ∀ (a a_1 : geographicalRegion), % 5.44/5.63 Eq (∀ (Z : geographicalRegion), And (subRegions a a_1) (subRegions a_1 Z) → subRegions a Z) True % 5.44/5.63 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.44/5.63 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : geographicalRegion), % 5.44/5.63 Or (Eq (And (subRegions a a_1) (subRegions a_1 a_2)) False) (Eq (subRegions a a_2) True) % 5.44/5.63 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : geographicalRegion), % 5.44/5.63 Or (Eq (subRegions a a_1) True) (Or (Eq (subRegions a a_2) False) (Eq (subRegions a_2 a_1) False)) % 5.44/5.63 Clause #82 (by superposition #[81, 9]): ∀ (a : geographicalRegion), % 5.44/5.63 Or (Eq (subRegions france a) True) (Or (Eq (subRegions hautsDeFrance a) False) (Eq False True)) % 5.44/5.63 Clause #83 (by superposition #[81, 8]): ∀ (a : geographicalRegion), % 5.44/5.63 Or (Eq (subRegions hautsDeFrance a) True) (Or (Eq (subRegions picardy a) False) (Eq False True)) % 5.44/5.63 Clause #85 (by superposition #[36, 60]): ∀ (a : event), % 5.44/5.63 Or (Eq (endsBeforeStartOf armistice1918 a) True) (Or (Eq (endsBeforeStartOf armistice1940 a) False) (Eq False True)) % 5.44/5.63 Clause #86 (by clausification #[6]): ∀ (a : geographicalRegion), % 5.44/5.63 Eq (∀ (Y : geographicalRegion) (Z : event), And (eventOccursAt Z a) (subRegions Y a) → eventOccursAt Z Y) True % 5.44/5.63 Clause #87 (by clausification #[86]): ∀ (a a_1 : geographicalRegion), % 5.44/5.63 Eq (∀ (Z : event), And (eventOccursAt Z a) (subRegions a_1 a) → eventOccursAt Z a_1) True % 5.44/5.63 Clause #88 (by clausification #[87]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.44/5.63 Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1) → eventOccursAt a a_2) True % 5.44/5.63 Clause #89 (by clausification #[88]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.44/5.63 Or (Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1)) False) (Eq (eventOccursAt a a_2) True) % 5.44/5.63 Clause #90 (by clausification #[89]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 5.44/5.63 Or (Eq (eventOccursAt a a_1) True) (Or (Eq (eventOccursAt a a_2) False) (Eq (subRegions a_1 a_2) False)) % 5.44/5.63 Clause #92 (by superposition #[90, 19]): ∀ (a : geographicalRegion), % 5.44/5.63 Or (Eq (eventOccursAt armistice1918 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 5.44/5.63 Clause #93 (by superposition #[90, 47]): ∀ (a : geographicalRegion), % 5.44/5.63 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 5.44/5.63 Clause #94 (by clausification #[10]): ∀ (a : constrCont), % 5.44/5.63 Eq (∀ (PR LT BW : govt), And (narrativeSuccessor a PR BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a PR LT) % 5.44/5.63 True % 5.44/5.63 Clause #95 (by clausification #[94]): ∀ (a : constrCont) (a_1 : govt), % 5.44/5.63 Eq (∀ (LT BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a a_1 LT) % 5.44/5.63 True % 5.44/5.63 Clause #96 (by clausification #[95]): ∀ (a : constrCont) (a_1 a_2 : govt), % 5.44/5.63 Eq (∀ (BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW a_2) → narrativeSuccessor a a_1 a_2) % 5.44/5.63 True % 5.44/5.63 Clause #97 (by clausification #[96]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.44/5.65 Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3) → narrativeSuccessor a a_1 a_3) True % 5.44/5.65 Clause #98 (by clausification #[97]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.44/5.65 Or (Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3)) False) % 5.44/5.65 (Eq (narrativeSuccessor a a_1 a_3) True) % 5.44/5.65 Clause #99 (by clausification #[98]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 5.44/5.65 Or (Eq (narrativeSuccessor a a_1 a_2) True) % 5.44/5.65 (Or (Eq (narrativeSuccessor a a_1 a_3) False) (Eq (narrativeSuccessor a a_3 a_2) False)) % 5.44/5.65 Clause #107 (by clausification #[71]): Eq (contentiousEvent armistice1918) True % 5.44/5.65 Clause #109 (by superposition #[16, 99]): ∀ (a : govt), % 5.44/5.65 Or (Eq (narrativeSuccessor marianne thirdRepublicFrench a) True) % 5.44/5.65 (Or (Eq (narrativeSuccessor marianne fourthRepublicFrench a) False) (Eq False True)) % 5.44/5.65 Clause #111 (by clausification #[75]): Eq (diplomaticEvent armistice1918) True % 5.44/5.65 Clause #112 (by clausification #[55]): Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) False % 5.44/5.65 Clause #113 (by clausification #[53]): ∀ (a : event), % 5.44/5.65 Eq % 5.44/5.65 (∀ (VE : event) (LOC : geographicalRegion), % 5.44/5.65 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf a VE) → % 5.44/5.65 pastColocatedDiplomaticEvent VE a) % 5.44/5.65 True % 5.44/5.65 Clause #114 (by clausification #[113]): ∀ (a a_1 : event), % 5.44/5.65 Eq % 5.44/5.65 (∀ (LOC : geographicalRegion), % 5.44/5.65 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt a_1 LOC)) (endsBeforeStartOf a a_1) → % 5.44/5.65 pastColocatedDiplomaticEvent a_1 a) % 5.44/5.65 True % 5.44/5.65 Clause #115 (by clausification #[114]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 5.44/5.65 Eq % 5.44/5.65 (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2) → % 5.44/5.65 pastColocatedDiplomaticEvent a_2 a) % 5.44/5.65 True % 5.44/5.65 Clause #116 (by clausification #[115]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 5.44/5.65 Or % 5.44/5.65 (Eq (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2)) % 5.44/5.65 False) % 5.44/5.65 (Eq (pastColocatedDiplomaticEvent a_2 a) True) % 5.44/5.65 Clause #117 (by clausification #[116]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.44/5.65 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.44/5.65 (Or (Eq (And (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) (eventOccursAt a a_2)) False) % 5.44/5.65 (Eq (endsBeforeStartOf a_1 a) False)) % 5.44/5.65 Clause #118 (by clausification #[117]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.44/5.65 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.44/5.65 (Or (Eq (endsBeforeStartOf a_1 a) False) % 5.44/5.65 (Or (Eq (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) False) (Eq (eventOccursAt a a_2) False))) % 5.44/5.65 Clause #119 (by clausification #[118]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 5.44/5.65 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 5.44/5.65 (Or (Eq (endsBeforeStartOf a_1 a) False) % 5.44/5.65 (Or (Eq (eventOccursAt a a_2) False) (Or (Eq (diplomaticEvent a_1) False) (Eq (eventOccursAt a_1 a_2) False)))) % 5.44/5.65 Clause #122 (by clausification #[93]): ∀ (a : geographicalRegion), % 5.44/5.65 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a rethondesCompiegne) False) % 5.44/5.65 Clause #123 (by superposition #[122, 7]): Or (Eq (eventOccursAt compiegneVisit2018 picardy) True) (Eq False True) % 5.44/5.65 Clause #124 (by clausification #[123]): Eq (eventOccursAt compiegneVisit2018 picardy) True % 5.44/5.65 Clause #125 (by superposition #[124, 90]): ∀ (a : geographicalRegion), % 5.44/5.65 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a picardy) False)) % 5.44/5.65 Clause #126 (by clausification #[125]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a picardy) False) % 5.44/5.65 Clause #127 (by superposition #[126, 8]): Or (Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True) (Eq False True) % 5.44/5.65 Clause #128 (by clausification #[127]): Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True % 5.44/5.65 Clause #129 (by superposition #[128, 90]): ∀ (a : geographicalRegion), % 5.44/5.65 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a hautsDeFrance) False)) % 5.44/5.67 Clause #130 (by clausification #[129]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a hautsDeFrance) False) % 5.44/5.67 Clause #131 (by superposition #[130, 9]): Or (Eq (eventOccursAt compiegneVisit2018 france) True) (Eq False True) % 5.44/5.67 Clause #132 (by clausification #[54]): ∀ (a : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.67 (seatingEvent SE)) % 5.44/5.67 (performedBy SE RP)) % 5.44/5.67 (seatedAtSide SE TS)) % 5.44/5.67 (govtRepresentedBy DE PASTGOVT RP)) % 5.44/5.67 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.44/5.67 (friendlyEvent VE)) % 5.44/5.67 (govtRepresentedBy VE GOVT a) → % 5.44/5.67 avoidTableSide a VE TS) % 5.44/5.67 True % 5.44/5.67 Clause #133 (by clausification #[132]): ∀ (a a_1 : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.67 (seatingEvent SE)) % 5.44/5.67 (performedBy SE a)) % 5.44/5.67 (seatedAtSide SE TS)) % 5.44/5.67 (govtRepresentedBy DE PASTGOVT a)) % 5.44/5.67 (narrativeSuccessor CC PASTGOVT GOVT)) % 5.44/5.67 (friendlyEvent VE)) % 5.44/5.67 (govtRepresentedBy VE GOVT a_1) → % 5.44/5.67 avoidTableSide a_1 VE TS) % 5.44/5.67 True % 5.44/5.67 Clause #134 (by clausification #[133]): ∀ (a : person) (a_1 : govt) (a_2 : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.67 (seatingEvent SE)) % 5.44/5.67 (performedBy SE a)) % 5.44/5.67 (seatedAtSide SE TS)) % 5.44/5.67 (govtRepresentedBy DE a_1 a)) % 5.44/5.67 (narrativeSuccessor CC a_1 GOVT)) % 5.44/5.67 (friendlyEvent VE)) % 5.44/5.67 (govtRepresentedBy VE GOVT a_2) → % 5.44/5.67 avoidTableSide a_2 VE TS) % 5.44/5.67 True % 5.44/5.67 Clause #135 (by clausification #[134]): ∀ (a : person) (a_1 a_2 : govt) (a_3 : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (CC : constrCont) (VE DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.67 (seatingEvent SE)) % 5.44/5.67 (performedBy SE a)) % 5.44/5.67 (seatedAtSide SE TS)) % 5.44/5.67 (govtRepresentedBy DE a_1 a)) % 5.44/5.67 (narrativeSuccessor CC a_1 a_2)) % 5.44/5.67 (friendlyEvent VE)) % 5.44/5.67 (govtRepresentedBy VE a_2 a_3) → % 5.44/5.67 avoidTableSide a_3 VE TS) % 5.44/5.67 True % 5.44/5.67 Clause #136 (by clausification #[135]): ∀ (a : person) (a_1 : govt) (a_2 : constrCont) (a_3 : govt) (a_4 : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (VE DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And % 5.44/5.67 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.67 (seatingEvent SE)) % 5.44/5.67 (performedBy SE a)) % 5.44/5.67 (seatedAtSide SE TS)) % 5.44/5.67 (govtRepresentedBy DE a_1 a)) % 5.44/5.67 (narrativeSuccessor a_2 a_1 a_3)) % 5.44/5.67 (friendlyEvent VE)) % 5.44/5.67 (govtRepresentedBy VE a_3 a_4) → % 5.44/5.67 avoidTableSide a_4 VE TS) % 5.44/5.67 True % 5.44/5.67 Clause #137 (by clausification #[136]): ∀ (a : event) (a_1 : person) (a_2 : govt) (a_3 : constrCont) (a_4 : govt) (a_5 : person), % 5.44/5.67 Eq % 5.44/5.67 (∀ (DE SE : event) (TS : table_side), % 5.44/5.67 And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a DE) (contentiousEvent DE)) (subEvents DE SE)) % 5.44/5.68 (seatingEvent SE)) % 5.44/5.68 (performedBy SE a_1)) % 5.44/5.68 (seatedAtSide SE TS)) % 5.44/5.68 (govtRepresentedBy DE a_2 a_1)) % 5.44/5.68 (narrativeSuccessor a_3 a_2 a_4)) % 5.44/5.68 (friendlyEvent a)) % 5.44/5.68 (govtRepresentedBy a a_4 a_5) → % 5.44/5.68 avoidTableSide a_5 a TS) % 5.44/5.68 True % 5.44/5.68 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.44/5.68 Eq % 5.44/5.68 (∀ (SE : event) (TS : table_side), % 5.44/5.68 And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 SE)) % 5.44/5.68 (seatingEvent SE)) % 5.44/5.68 (performedBy SE a_2)) % 5.44/5.68 (seatedAtSide SE TS)) % 5.44/5.68 (govtRepresentedBy a_1 a_3 a_2)) % 5.44/5.68 (narrativeSuccessor a_4 a_3 a_5)) % 5.44/5.68 (friendlyEvent a)) % 5.44/5.68 (govtRepresentedBy a a_5 a_6) → % 5.44/5.68 avoidTableSide a_6 a TS) % 5.44/5.68 True % 5.44/5.68 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.44/5.68 Eq % 5.44/5.68 (∀ (TS : table_side), % 5.44/5.68 And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.44/5.68 (seatingEvent a_2)) % 5.44/5.68 (performedBy a_2 a_3)) % 5.44/5.68 (seatedAtSide a_2 TS)) % 5.44/5.68 (govtRepresentedBy a_1 a_4 a_3)) % 5.44/5.68 (narrativeSuccessor a_5 a_4 a_6)) % 5.44/5.68 (friendlyEvent a)) % 5.44/5.68 (govtRepresentedBy a a_6 a_7) → % 5.44/5.68 avoidTableSide a_7 a TS) % 5.44/5.68 True % 5.44/5.68 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.44/5.68 Eq % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.44/5.68 (seatingEvent a_2)) % 5.44/5.68 (performedBy a_2 a_3)) % 5.44/5.68 (seatedAtSide a_2 a_4)) % 5.44/5.68 (govtRepresentedBy a_1 a_5 a_3)) % 5.44/5.68 (narrativeSuccessor a_6 a_5 a_7)) % 5.44/5.68 (friendlyEvent a)) % 5.44/5.68 (govtRepresentedBy a a_7 a_8) → % 5.44/5.68 avoidTableSide a_8 a a_4) % 5.44/5.68 True % 5.44/5.68 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.44/5.68 Or % 5.44/5.68 (Eq % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 5.44/5.68 (seatingEvent a_2)) % 5.44/5.68 (performedBy a_2 a_3)) % 5.44/5.68 (seatedAtSide a_2 a_4)) % 5.44/5.68 (govtRepresentedBy a_1 a_5 a_3)) % 5.44/5.68 (narrativeSuccessor a_6 a_5 a_7)) % 5.44/5.68 (friendlyEvent a)) % 5.44/5.68 (govtRepresentedBy a a_7 a_8)) % 5.44/5.68 False) % 5.44/5.68 (Eq (avoidTableSide a_8 a a_4) True) % 5.44/5.68 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.44/5.68 (a_8 : govt), % 5.44/5.68 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.44/5.68 (Or % 5.44/5.68 (Eq % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And % 5.44/5.68 (And (And (And (pastColocatedDiplomaticEvent a_1 a_3) (contentiousEvent a_3)) (subEvents a_3 a_4)) % 5.44/5.68 (seatingEvent a_4)) % 5.44/5.68 (performedBy a_4 a_5)) % 5.44/5.68 (seatedAtSide a_4 a_2)) % 5.44/5.68 (govtRepresentedBy a_3 a_6 a_5)) % 5.44/5.68 (narrativeSuccessor a_7 a_6 a_8)) % 5.44/5.68 (friendlyEvent a_1)) % 5.54/5.70 False) % 5.54/5.70 (Eq (govtRepresentedBy a_1 a_8 a) False)) % 5.54/5.70 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.54/5.70 (a_8 : constrCont), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.70 (Or % 5.54/5.70 (Eq % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 5.54/5.70 (seatingEvent a_5)) % 5.54/5.70 (performedBy a_5 a_6)) % 5.54/5.70 (seatedAtSide a_5 a_2)) % 5.54/5.70 (govtRepresentedBy a_4 a_7 a_6)) % 5.54/5.70 (narrativeSuccessor a_8 a_7 a_3)) % 5.54/5.70 False) % 5.54/5.70 (Eq (friendlyEvent a_1) False))) % 5.54/5.70 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.54/5.70 (a_8 : constrCont), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.70 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.70 (Or % 5.54/5.70 (Eq % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 5.54/5.70 (seatingEvent a_5)) % 5.54/5.70 (performedBy a_5 a_6)) % 5.54/5.70 (seatedAtSide a_5 a_2)) % 5.54/5.70 (govtRepresentedBy a_4 a_7 a_6)) % 5.54/5.70 False) % 5.54/5.70 (Eq (narrativeSuccessor a_8 a_7 a_3) False)))) % 5.54/5.70 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.54/5.70 (a_8 : person), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.70 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.70 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.70 (Or % 5.54/5.70 (Eq % 5.54/5.70 (And % 5.54/5.70 (And % 5.54/5.70 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_7)) % 5.54/5.70 (seatingEvent a_7)) % 5.54/5.70 (performedBy a_7 a_8)) % 5.54/5.70 (seatedAtSide a_7 a_2)) % 5.54/5.70 False) % 5.54/5.70 (Eq (govtRepresentedBy a_6 a_5 a_8) False))))) % 5.54/5.70 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.54/5.70 (a_7 : person) (a_8 : event), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.70 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.70 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.54/5.70 (Or % 5.54/5.70 (Eq % 5.54/5.70 (And % 5.54/5.70 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.54/5.70 (seatingEvent a_8)) % 5.54/5.70 (performedBy a_8 a_7)) % 5.54/5.70 False) % 5.54/5.70 (Eq (seatedAtSide a_8 a_2) False)))))) % 5.54/5.70 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.54/5.70 (a_7 : person) (a_8 : event), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.70 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.70 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.54/5.70 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.54/5.70 (Or % 5.54/5.70 (Eq % 5.54/5.70 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.54/5.70 (seatingEvent a_8)) % 5.54/5.70 False) % 5.54/5.70 (Eq (performedBy a_8 a_7) False))))))) % 5.54/5.70 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.54/5.70 (a_7 : person) (a_8 : event), % 5.54/5.70 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.70 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.71 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.71 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.54/5.71 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.54/5.71 (Or (Eq (performedBy a_8 a_7) False) % 5.54/5.71 (Or % 5.54/5.71 (Eq (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 5.54/5.71 False) % 5.54/5.71 (Eq (seatingEvent a_8) False)))))))) % 5.54/5.71 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.54/5.71 (a_7 : person) (a_8 : event), % 5.54/5.71 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.71 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.71 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.54/5.71 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.54/5.71 (Or (Eq (performedBy a_8 a_7) False) % 5.54/5.71 (Or (Eq (seatingEvent a_8) False) % 5.54/5.71 (Or (Eq (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) False) % 5.54/5.71 (Eq (subEvents a_6 a_8) False))))))))) % 5.54/5.71 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.54/5.71 (a_7 : person) (a_8 : event), % 5.54/5.71 Or (Eq (avoidTableSide a a_1 a_2) True) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 5.54/5.71 (Or (Eq (friendlyEvent a_1) False) % 5.54/5.71 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 5.54/5.71 (Or (Eq (seatedAtSide a_8 a_2) False) % 5.54/5.71 (Or (Eq (performedBy a_8 a_7) False) % 5.54/5.71 (Or (Eq (seatingEvent a_8) False) % 5.54/5.71 (Or (Eq (subEvents a_6 a_8) False) % 5.54/5.71 (Or (Eq (pastColocatedDiplomaticEvent a_1 a_6) False) (Eq (contentiousEvent a_6) False)))))))))) % 5.54/5.71 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.54/5.71 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.71 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 5.54/5.71 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.54/5.71 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.54/5.71 (Or (Eq (seatedAtSide a_5 a) False) % 5.54/5.71 (Or (Eq (performedBy a_5 a_4) False) % 5.54/5.71 (Or (Eq (seatingEvent a_5) False) % 5.54/5.71 (Or (Eq (subEvents a_3 a_5) False) % 5.54/5.71 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.54/5.71 (Or (Eq (contentiousEvent a_3) False) (Eq False True)))))))))) % 5.54/5.71 Clause #157 (by clausification #[131]): Eq (eventOccursAt compiegneVisit2018 france) True % 5.54/5.71 Clause #160 (by clausification #[85]): ∀ (a : event), Or (Eq (endsBeforeStartOf armistice1918 a) True) (Eq (endsBeforeStartOf armistice1940 a) False) % 5.54/5.71 Clause #161 (by superposition #[160, 52]): Or (Eq (endsBeforeStartOf armistice1918 compiegneVisit2018) True) (Eq False True) % 5.54/5.71 Clause #162 (by clausification #[161]): Eq (endsBeforeStartOf armistice1918 compiegneVisit2018) True % 5.54/5.71 Clause #164 (by superposition #[162, 119]): ∀ (a : geographicalRegion), % 5.54/5.71 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.71 (Or (Eq True False) % 5.54/5.71 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 5.54/5.71 (Or (Eq (diplomaticEvent armistice1918) False) (Eq (eventOccursAt armistice1918 a) False)))) % 5.54/5.71 Clause #167 (by clausification #[82]): ∀ (a : geographicalRegion), Or (Eq (subRegions france a) True) (Eq (subRegions hautsDeFrance a) False) % 5.54/5.71 Clause #173 (by clausification #[83]): ∀ (a : geographicalRegion), Or (Eq (subRegions hautsDeFrance a) True) (Eq (subRegions picardy a) False) % 5.54/5.71 Clause #174 (by superposition #[173, 7]): Or (Eq (subRegions hautsDeFrance rethondesCompiegne) True) (Eq False True) % 5.54/5.71 Clause #179 (by clausification #[174]): Eq (subRegions hautsDeFrance rethondesCompiegne) True % 5.54/5.71 Clause #182 (by superposition #[179, 167]): Or (Eq (subRegions france rethondesCompiegne) True) (Eq True False) % 5.54/5.73 Clause #184 (by clausification #[182]): Eq (subRegions france rethondesCompiegne) True % 5.54/5.73 Clause #191 (by clausification #[92]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt armistice1918 a) True) (Eq (subRegions a rethondesCompiegne) False) % 5.54/5.73 Clause #194 (by superposition #[191, 184]): Or (Eq (eventOccursAt armistice1918 france) True) (Eq False True) % 5.54/5.73 Clause #195 (by clausification #[194]): Eq (eventOccursAt armistice1918 france) True % 5.54/5.73 Clause #248 (by clausification #[109]): ∀ (a : govt), % 5.54/5.73 Or (Eq (narrativeSuccessor marianne thirdRepublicFrench a) True) % 5.54/5.73 (Eq (narrativeSuccessor marianne fourthRepublicFrench a) False) % 5.54/5.73 Clause #249 (by superposition #[248, 17]): Or (Eq (narrativeSuccessor marianne thirdRepublicFrench fifthRepublicFrench) True) (Eq False True) % 5.54/5.73 Clause #250 (by clausification #[249]): Eq (narrativeSuccessor marianne thirdRepublicFrench fifthRepublicFrench) True % 5.54/5.73 Clause #259 (by clausification #[164]): ∀ (a : geographicalRegion), % 5.54/5.73 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.73 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 5.54/5.73 (Or (Eq (diplomaticEvent armistice1918) False) (Eq (eventOccursAt armistice1918 a) False))) % 5.54/5.73 Clause #260 (by forward demodulation #[259, 111]): ∀ (a : geographicalRegion), % 5.54/5.73 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.73 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Or (Eq True False) (Eq (eventOccursAt armistice1918 a) False))) % 5.54/5.73 Clause #261 (by clausification #[260]): ∀ (a : geographicalRegion), % 5.54/5.73 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.73 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Eq (eventOccursAt armistice1918 a) False)) % 5.54/5.73 Clause #265 (by superposition #[261, 157]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.73 (Or (Eq (eventOccursAt armistice1918 france) False) (Eq False True)) % 5.54/5.73 Clause #266 (by clausification #[265]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 5.54/5.73 (Eq (eventOccursAt armistice1918 france) False) % 5.54/5.73 Clause #267 (by forward demodulation #[266, 195]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) (Eq True False) % 5.54/5.73 Clause #268 (by clausification #[267]): Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True % 5.54/5.73 Clause #369 (by clausification #[155]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.54/5.73 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.73 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 5.54/5.73 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.54/5.73 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.54/5.73 (Or (Eq (seatedAtSide a_5 a) False) % 5.54/5.73 (Or (Eq (performedBy a_5 a_4) False) % 5.54/5.73 (Or (Eq (seatingEvent a_5) False) % 5.54/5.73 (Or (Eq (subEvents a_3 a_5) False) % 5.54/5.73 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.54/5.73 (Eq (contentiousEvent a_3) False))))))))) % 5.54/5.73 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.54/5.73 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.73 (Or (Eq True False) % 5.54/5.73 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.54/5.73 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.54/5.73 (Or (Eq (seatedAtSide a_5 a) False) % 5.54/5.73 (Or (Eq (performedBy a_5 a_4) False) % 5.54/5.73 (Or (Eq (seatingEvent a_5) False) % 5.54/5.73 (Or (Eq (subEvents a_3 a_5) False) % 5.54/5.73 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.54/5.73 (Eq (contentiousEvent a_3) False))))))))) % 5.54/5.73 Clause #371 (by clausification #[370]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 5.54/5.73 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.73 (Or (Eq (narrativeSuccessor a_1 a_2 fifthRepublicFrench) False) % 5.54/5.73 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 5.54/5.75 (Or (Eq (seatedAtSide a_5 a) False) % 5.54/5.75 (Or (Eq (performedBy a_5 a_4) False) % 5.54/5.75 (Or (Eq (seatingEvent a_5) False) % 5.54/5.75 (Or (Eq (subEvents a_3 a_5) False) % 5.54/5.75 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 5.54/5.75 (Eq (contentiousEvent a_3) False)))))))) % 5.54/5.75 Clause #374 (by superposition #[371, 250]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (govtRepresentedBy a_1 thirdRepublicFrench a_2) False) % 5.54/5.75 (Or (Eq (seatedAtSide a_3 a) False) % 5.54/5.75 (Or (Eq (performedBy a_3 a_2) False) % 5.54/5.75 (Or (Eq (seatingEvent a_3) False) % 5.54/5.75 (Or (Eq (subEvents a_1 a_3) False) % 5.54/5.75 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 5.54/5.75 (Or (Eq (contentiousEvent a_1) False) (Eq False True)))))))) % 5.54/5.75 Clause #375 (by clausification #[374]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (govtRepresentedBy a_1 thirdRepublicFrench a_2) False) % 5.54/5.75 (Or (Eq (seatedAtSide a_3 a) False) % 5.54/5.75 (Or (Eq (performedBy a_3 a_2) False) % 5.54/5.75 (Or (Eq (seatingEvent a_3) False) % 5.54/5.75 (Or (Eq (subEvents a_1 a_3) False) % 5.54/5.75 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 5.54/5.75 (Eq (contentiousEvent a_1) False))))))) % 5.54/5.75 Clause #376 (by superposition #[375, 20]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) % 5.54/5.75 (Or (Eq (subEvents armistice1918 a_1) False) % 5.54/5.75 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) False) % 5.54/5.75 (Or (Eq (contentiousEvent armistice1918) False) (Eq False True))))))) % 5.54/5.75 Clause #406 (by clausification #[376]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) % 5.54/5.75 (Or (Eq (subEvents armistice1918 a_1) False) % 5.54/5.75 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) False) % 5.54/5.75 (Eq (contentiousEvent armistice1918) False)))))) % 5.54/5.75 Clause #407 (by forward demodulation #[406, 268]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) % 5.54/5.75 (Or (Eq (subEvents armistice1918 a_1) False) % 5.54/5.75 (Or (Eq True False) (Eq (contentiousEvent armistice1918) False)))))) % 5.54/5.75 Clause #408 (by clausification #[407]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) % 5.54/5.75 (Or (Eq (subEvents armistice1918 a_1) False) (Eq (contentiousEvent armistice1918) False))))) % 5.54/5.75 Clause #409 (by forward demodulation #[408, 107]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) (Or (Eq (subEvents armistice1918 a_1) False) (Eq True False))))) % 5.54/5.75 Clause #410 (by clausification #[409]): ∀ (a : table_side) (a_1 : event), % 5.54/5.75 Or (Eq (avoidTableSide macron compiegneVisit2018 a) True) % 5.54/5.75 (Or (Eq (seatedAtSide a_1 a) False) % 5.54/5.75 (Or (Eq (performedBy a_1 foch) False) % 5.54/5.75 (Or (Eq (seatingEvent a_1) False) (Eq (subEvents armistice1918 a_1) False)))) % 5.54/5.75 Clause #412 (by superposition #[410, 25]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Or (Eq (performedBy armistice1918AlliedSeating foch) False) % 5.54/5.75 (Or (Eq (seatingEvent armistice1918AlliedSeating) False) % 5.54/5.75 (Or (Eq (subEvents armistice1918 armistice1918AlliedSeating) False) (Eq False True)))) % 5.54/5.75 Clause #422 (by clausification #[412]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Or (Eq (performedBy armistice1918AlliedSeating foch) False) % 5.54/5.75 (Or (Eq (seatingEvent armistice1918AlliedSeating) False) % 5.54/5.75 (Eq (subEvents armistice1918 armistice1918AlliedSeating) False))) % 5.54/5.75 Clause #423 (by forward demodulation #[422, 24]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Or (Eq True False) % 5.54/5.75 (Or (Eq (seatingEvent armistice1918AlliedSeating) False) % 5.54/5.75 (Eq (subEvents armistice1918 armistice1918AlliedSeating) False))) % 5.54/5.75 Clause #424 (by clausification #[423]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Or (Eq (seatingEvent armistice1918AlliedSeating) False) % 5.54/5.75 (Eq (subEvents armistice1918 armistice1918AlliedSeating) False)) % 5.54/5.75 Clause #425 (by forward demodulation #[424, 22]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Or (Eq True False) (Eq (subEvents armistice1918 armistice1918AlliedSeating) False)) % 5.54/5.75 Clause #426 (by clausification #[425]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) % 5.54/5.75 (Eq (subEvents armistice1918 armistice1918AlliedSeating) False) % 5.54/5.75 Clause #427 (by forward demodulation #[426, 23]): Or (Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True) (Eq True False) % 5.54/5.75 Clause #428 (by clausification #[427]): Eq (avoidTableSide macron compiegneVisit2018 cwlTableSideA) True % 5.54/5.75 Clause #429 (by superposition #[428, 112]): Eq True False % 5.54/5.75 Clause #430 (by clausification #[429]): False % 5.54/5.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------