%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ160_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 4.74s 4.94s % Output : Proof 4.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PUZ160_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.15/0.33 % Computer : n013.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 05:00:25 EDT 2026 % 0.15/0.33 % CPUTime : % 4.74/4.94 SZS status Theorem for theBenchmark.p % 4.74/4.94 SZS output start Proof for theBenchmark.p % 4.74/4.94 Clause #0 (by assumption #[]): Eq (∀ (X Y Z : event), And (endsBeforeStartOf X Y) (endsBeforeStartOf Y Z) → endsBeforeStartOf X Z) True % 4.74/4.94 Clause #3 (by assumption #[]): Eq (∀ (E : event), armistice E → contentiousEvent E) True % 4.74/4.94 Clause #4 (by assumption #[]): Eq (∀ (E : event), armistice E → diplomaticEvent E) True % 4.74/4.94 Clause #5 (by assumption #[]): Eq (∀ (X Y Z : geographicalRegion), And (subRegions X Y) (subRegions Y Z) → subRegions X Z) True % 4.74/4.94 Clause #6 (by assumption #[]): Eq (∀ (X Y : geographicalRegion) (Z : event), And (eventOccursAt Z X) (subRegions Y X) → eventOccursAt Z Y) True % 4.74/4.94 Clause #7 (by assumption #[]): Eq (subRegions picardy rethondesCompiegne) True % 4.74/4.94 Clause #8 (by assumption #[]): Eq (subRegions hautsDeFrance picardy) True % 4.74/4.94 Clause #9 (by assumption #[]): Eq (subRegions france hautsDeFrance) True % 4.74/4.94 Clause #10 (by assumption #[]): Eq % 4.74/4.94 (∀ (CC : constrCont) (PR LT BW : govt), % 4.74/4.94 And (narrativeSuccessor CC PR BW) (narrativeSuccessor CC BW LT) → narrativeSuccessor CC PR LT) % 4.74/4.94 True % 4.74/4.94 Clause #11 (by assumption #[]): Eq (narrativeSuccessor germania germanEmpire weimarRepublic) True % 4.74/4.94 Clause #12 (by assumption #[]): Eq (narrativeSuccessor germania weimarRepublic thirdReich) True % 4.74/4.94 Clause #13 (by assumption #[]): Eq (narrativeSuccessor germania thirdReich alliedOccupiedGermany) True % 4.74/4.94 Clause #14 (by assumption #[]): Eq (narrativeSuccessor germania alliedOccupiedGermany federalGermanRepublic) True % 4.74/4.94 Clause #18 (by assumption #[]): Eq (armistice armistice1918) True % 4.74/4.94 Clause #19 (by assumption #[]): Eq (eventOccursAt armistice1918 rethondesCompiegne) True % 4.74/4.94 Clause #21 (by assumption #[]): Eq (govtRepresentedBy armistice1918 germanEmpire erzberger) True % 4.74/4.94 Clause #27 (by assumption #[]): Eq (seatingEvent armistice1918GermanSeating) True % 4.74/4.94 Clause #28 (by assumption #[]): Eq (subEvents armistice1918 armistice1918GermanSeating) True % 4.74/4.94 Clause #29 (by assumption #[]): Eq (performedBy armistice1918GermanSeating erzberger) True % 4.74/4.94 Clause #30 (by assumption #[]): Eq (seatedAtSide armistice1918GermanSeating cwlTableSideC) True % 4.74/4.94 Clause #36 (by assumption #[]): Eq (endsBeforeStartOf armistice1918 armistice1940) True % 4.74/4.94 Clause #47 (by assumption #[]): Eq (eventOccursAt compiegneVisit2018 rethondesCompiegne) True % 4.74/4.94 Clause #49 (by assumption #[]): Eq (friendlyEvent compiegneVisit2018) True % 4.74/4.94 Clause #50 (by assumption #[]): Eq (govtRepresentedBy compiegneVisit2018 federalGermanRepublic merkel) True % 4.74/4.94 Clause #52 (by assumption #[]): Eq (endsBeforeStartOf armistice1940 compiegneVisit2018) True % 4.74/4.94 Clause #53 (by assumption #[]): Eq % 4.74/4.94 (∀ (DE VE : event) (LOC : geographicalRegion), % 4.74/4.94 And (And (And (diplomaticEvent DE) (eventOccursAt DE LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf DE VE) → % 4.74/4.94 pastColocatedDiplomaticEvent VE DE) % 4.74/4.94 True % 4.74/4.94 Clause #54 (by assumption #[]): Eq % 4.74/4.94 (∀ (P RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.74/4.94 And % 4.74/4.94 (And % 4.74/4.94 (And % 4.74/4.94 (And % 4.74/4.94 (And % 4.74/4.94 (And % 4.74/4.94 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.94 (seatingEvent SE)) % 4.74/4.94 (performedBy SE RP)) % 4.74/4.94 (seatedAtSide SE TS)) % 4.74/4.94 (govtRepresentedBy DE PASTGOVT RP)) % 4.74/4.94 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.74/4.94 (friendlyEvent VE)) % 4.74/4.94 (govtRepresentedBy VE GOVT P) → % 4.74/4.94 avoidTableSide P VE TS) % 4.74/4.94 True % 4.74/4.94 Clause #55 (by assumption #[]): Eq (Not (avoidTableSide merkel compiegneVisit2018 cwlTableSideC)) True % 4.74/4.94 Clause #56 (by clausification #[0]): ∀ (a : event), Eq (∀ (Y Z : event), And (endsBeforeStartOf a Y) (endsBeforeStartOf Y Z) → endsBeforeStartOf a Z) True % 4.74/4.94 Clause #57 (by clausification #[56]): ∀ (a a_1 : event), % 4.74/4.94 Eq (∀ (Z : event), And (endsBeforeStartOf a a_1) (endsBeforeStartOf a_1 Z) → endsBeforeStartOf a Z) True % 4.74/4.94 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 % 4.74/4.94 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : event), % 4.74/4.96 Or (Eq (And (endsBeforeStartOf a a_1) (endsBeforeStartOf a_1 a_2)) False) (Eq (endsBeforeStartOf a a_2) True) % 4.74/4.96 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 : event), % 4.74/4.96 Or (Eq (endsBeforeStartOf a a_1) True) % 4.74/4.96 (Or (Eq (endsBeforeStartOf a a_2) False) (Eq (endsBeforeStartOf a_2 a_1) False)) % 4.74/4.96 Clause #68 (by clausification #[3]): ∀ (a : event), Eq (armistice a → contentiousEvent a) True % 4.74/4.96 Clause #69 (by clausification #[68]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (contentiousEvent a) True) % 4.74/4.96 Clause #71 (by superposition #[69, 18]): Or (Eq (contentiousEvent armistice1918) True) (Eq False True) % 4.74/4.96 Clause #72 (by clausification #[4]): ∀ (a : event), Eq (armistice a → diplomaticEvent a) True % 4.74/4.96 Clause #73 (by clausification #[72]): ∀ (a : event), Or (Eq (armistice a) False) (Eq (diplomaticEvent a) True) % 4.74/4.96 Clause #75 (by superposition #[73, 18]): Or (Eq (diplomaticEvent armistice1918) True) (Eq False True) % 4.74/4.96 Clause #77 (by clausification #[5]): ∀ (a : geographicalRegion), % 4.74/4.96 Eq (∀ (Y Z : geographicalRegion), And (subRegions a Y) (subRegions Y Z) → subRegions a Z) True % 4.74/4.96 Clause #78 (by clausification #[77]): ∀ (a a_1 : geographicalRegion), % 4.74/4.96 Eq (∀ (Z : geographicalRegion), And (subRegions a a_1) (subRegions a_1 Z) → subRegions a Z) True % 4.74/4.96 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 % 4.74/4.96 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : geographicalRegion), % 4.74/4.96 Or (Eq (And (subRegions a a_1) (subRegions a_1 a_2)) False) (Eq (subRegions a a_2) True) % 4.74/4.96 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 : geographicalRegion), % 4.74/4.96 Or (Eq (subRegions a a_1) True) (Or (Eq (subRegions a a_2) False) (Eq (subRegions a_2 a_1) False)) % 4.74/4.96 Clause #82 (by superposition #[81, 9]): ∀ (a : geographicalRegion), % 4.74/4.96 Or (Eq (subRegions france a) True) (Or (Eq (subRegions hautsDeFrance a) False) (Eq False True)) % 4.74/4.96 Clause #83 (by superposition #[81, 8]): ∀ (a : geographicalRegion), % 4.74/4.96 Or (Eq (subRegions hautsDeFrance a) True) (Or (Eq (subRegions picardy a) False) (Eq False True)) % 4.74/4.96 Clause #85 (by superposition #[36, 60]): ∀ (a : event), % 4.74/4.96 Or (Eq (endsBeforeStartOf armistice1918 a) True) (Or (Eq (endsBeforeStartOf armistice1940 a) False) (Eq False True)) % 4.74/4.96 Clause #86 (by clausification #[6]): ∀ (a : geographicalRegion), % 4.74/4.96 Eq (∀ (Y : geographicalRegion) (Z : event), And (eventOccursAt Z a) (subRegions Y a) → eventOccursAt Z Y) True % 4.74/4.96 Clause #87 (by clausification #[86]): ∀ (a a_1 : geographicalRegion), % 4.74/4.96 Eq (∀ (Z : event), And (eventOccursAt Z a) (subRegions a_1 a) → eventOccursAt Z a_1) True % 4.74/4.96 Clause #88 (by clausification #[87]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.74/4.96 Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1) → eventOccursAt a a_2) True % 4.74/4.96 Clause #89 (by clausification #[88]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.74/4.96 Or (Eq (And (eventOccursAt a a_1) (subRegions a_2 a_1)) False) (Eq (eventOccursAt a a_2) True) % 4.74/4.96 Clause #90 (by clausification #[89]): ∀ (a : event) (a_1 a_2 : geographicalRegion), % 4.74/4.96 Or (Eq (eventOccursAt a a_1) True) (Or (Eq (eventOccursAt a a_2) False) (Eq (subRegions a_1 a_2) False)) % 4.74/4.96 Clause #92 (by superposition #[90, 19]): ∀ (a : geographicalRegion), % 4.74/4.96 Or (Eq (eventOccursAt armistice1918 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 4.74/4.96 Clause #93 (by superposition #[90, 47]): ∀ (a : geographicalRegion), % 4.74/4.96 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq (subRegions a rethondesCompiegne) False) (Eq False True)) % 4.74/4.96 Clause #94 (by clausification #[10]): ∀ (a : constrCont), % 4.74/4.96 Eq (∀ (PR LT BW : govt), And (narrativeSuccessor a PR BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a PR LT) % 4.74/4.96 True % 4.74/4.96 Clause #95 (by clausification #[94]): ∀ (a : constrCont) (a_1 : govt), % 4.74/4.96 Eq (∀ (LT BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW LT) → narrativeSuccessor a a_1 LT) % 4.74/4.96 True % 4.74/4.96 Clause #96 (by clausification #[95]): ∀ (a : constrCont) (a_1 a_2 : govt), % 4.74/4.96 Eq (∀ (BW : govt), And (narrativeSuccessor a a_1 BW) (narrativeSuccessor a BW a_2) → narrativeSuccessor a a_1 a_2) % 4.74/4.98 True % 4.74/4.98 Clause #97 (by clausification #[96]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.74/4.98 Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3) → narrativeSuccessor a a_1 a_3) True % 4.74/4.98 Clause #98 (by clausification #[97]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.74/4.98 Or (Eq (And (narrativeSuccessor a a_1 a_2) (narrativeSuccessor a a_2 a_3)) False) % 4.74/4.98 (Eq (narrativeSuccessor a a_1 a_3) True) % 4.74/4.98 Clause #99 (by clausification #[98]): ∀ (a : constrCont) (a_1 a_2 a_3 : govt), % 4.74/4.98 Or (Eq (narrativeSuccessor a a_1 a_2) True) % 4.74/4.98 (Or (Eq (narrativeSuccessor a a_1 a_3) False) (Eq (narrativeSuccessor a a_3 a_2) False)) % 4.74/4.98 Clause #102 (by superposition #[99, 11]): ∀ (a : govt), % 4.74/4.98 Or (Eq (narrativeSuccessor germania germanEmpire a) True) % 4.74/4.98 (Or (Eq (narrativeSuccessor germania weimarRepublic a) False) (Eq False True)) % 4.74/4.98 Clause #103 (by superposition #[99, 13]): ∀ (a : govt), % 4.74/4.98 Or (Eq (narrativeSuccessor germania thirdReich a) True) % 4.74/4.98 (Or (Eq (narrativeSuccessor germania alliedOccupiedGermany a) False) (Eq False True)) % 4.74/4.98 Clause #107 (by clausification #[71]): Eq (contentiousEvent armistice1918) True % 4.74/4.98 Clause #111 (by clausification #[75]): Eq (diplomaticEvent armistice1918) True % 4.74/4.98 Clause #112 (by clausification #[55]): Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) False % 4.74/4.98 Clause #113 (by clausification #[53]): ∀ (a : event), % 4.74/4.98 Eq % 4.74/4.98 (∀ (VE : event) (LOC : geographicalRegion), % 4.74/4.98 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt VE LOC)) (endsBeforeStartOf a VE) → % 4.74/4.98 pastColocatedDiplomaticEvent VE a) % 4.74/4.98 True % 4.74/4.98 Clause #114 (by clausification #[113]): ∀ (a a_1 : event), % 4.74/4.98 Eq % 4.74/4.98 (∀ (LOC : geographicalRegion), % 4.74/4.98 And (And (And (diplomaticEvent a) (eventOccursAt a LOC)) (eventOccursAt a_1 LOC)) (endsBeforeStartOf a a_1) → % 4.74/4.98 pastColocatedDiplomaticEvent a_1 a) % 4.74/4.98 True % 4.74/4.98 Clause #115 (by clausification #[114]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 4.74/4.98 Eq % 4.74/4.98 (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2) → % 4.74/4.98 pastColocatedDiplomaticEvent a_2 a) % 4.74/4.98 True % 4.74/4.98 Clause #116 (by clausification #[115]): ∀ (a : event) (a_1 : geographicalRegion) (a_2 : event), % 4.74/4.98 Or % 4.74/4.98 (Eq (And (And (And (diplomaticEvent a) (eventOccursAt a a_1)) (eventOccursAt a_2 a_1)) (endsBeforeStartOf a a_2)) % 4.74/4.98 False) % 4.74/4.98 (Eq (pastColocatedDiplomaticEvent a_2 a) True) % 4.74/4.98 Clause #117 (by clausification #[116]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.74/4.98 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.74/4.98 (Or (Eq (And (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) (eventOccursAt a a_2)) False) % 4.74/4.98 (Eq (endsBeforeStartOf a_1 a) False)) % 4.74/4.98 Clause #118 (by clausification #[117]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.74/4.98 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.74/4.98 (Or (Eq (endsBeforeStartOf a_1 a) False) % 4.74/4.98 (Or (Eq (And (diplomaticEvent a_1) (eventOccursAt a_1 a_2)) False) (Eq (eventOccursAt a a_2) False))) % 4.74/4.98 Clause #119 (by clausification #[118]): ∀ (a a_1 : event) (a_2 : geographicalRegion), % 4.74/4.98 Or (Eq (pastColocatedDiplomaticEvent a a_1) True) % 4.74/4.98 (Or (Eq (endsBeforeStartOf a_1 a) False) % 4.74/4.98 (Or (Eq (eventOccursAt a a_2) False) (Or (Eq (diplomaticEvent a_1) False) (Eq (eventOccursAt a_1 a_2) False)))) % 4.74/4.98 Clause #122 (by clausification #[93]): ∀ (a : geographicalRegion), % 4.74/4.98 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a rethondesCompiegne) False) % 4.74/4.98 Clause #123 (by superposition #[122, 7]): Or (Eq (eventOccursAt compiegneVisit2018 picardy) True) (Eq False True) % 4.74/4.98 Clause #124 (by clausification #[123]): Eq (eventOccursAt compiegneVisit2018 picardy) True % 4.74/4.98 Clause #125 (by superposition #[124, 90]): ∀ (a : geographicalRegion), % 4.74/4.98 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a picardy) False)) % 4.74/4.98 Clause #126 (by clausification #[125]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a picardy) False) % 4.74/4.99 Clause #127 (by superposition #[126, 8]): Or (Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True) (Eq False True) % 4.74/4.99 Clause #128 (by clausification #[127]): Eq (eventOccursAt compiegneVisit2018 hautsDeFrance) True % 4.74/4.99 Clause #129 (by superposition #[128, 90]): ∀ (a : geographicalRegion), % 4.74/4.99 Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Or (Eq True False) (Eq (subRegions a hautsDeFrance) False)) % 4.74/4.99 Clause #130 (by clausification #[129]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt compiegneVisit2018 a) True) (Eq (subRegions a hautsDeFrance) False) % 4.74/4.99 Clause #131 (by superposition #[130, 9]): Or (Eq (eventOccursAt compiegneVisit2018 france) True) (Eq False True) % 4.74/4.99 Clause #132 (by clausification #[54]): ∀ (a : person), % 4.74/4.99 Eq % 4.74/4.99 (∀ (RP : person) (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.74/4.99 And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.99 (seatingEvent SE)) % 4.74/4.99 (performedBy SE RP)) % 4.74/4.99 (seatedAtSide SE TS)) % 4.74/4.99 (govtRepresentedBy DE PASTGOVT RP)) % 4.74/4.99 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.74/4.99 (friendlyEvent VE)) % 4.74/4.99 (govtRepresentedBy VE GOVT a) → % 4.74/4.99 avoidTableSide a VE TS) % 4.74/4.99 True % 4.74/4.99 Clause #133 (by clausification #[132]): ∀ (a a_1 : person), % 4.74/4.99 Eq % 4.74/4.99 (∀ (PASTGOVT GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.74/4.99 And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.99 (seatingEvent SE)) % 4.74/4.99 (performedBy SE a)) % 4.74/4.99 (seatedAtSide SE TS)) % 4.74/4.99 (govtRepresentedBy DE PASTGOVT a)) % 4.74/4.99 (narrativeSuccessor CC PASTGOVT GOVT)) % 4.74/4.99 (friendlyEvent VE)) % 4.74/4.99 (govtRepresentedBy VE GOVT a_1) → % 4.74/4.99 avoidTableSide a_1 VE TS) % 4.74/4.99 True % 4.74/4.99 Clause #134 (by clausification #[133]): ∀ (a : person) (a_1 : govt) (a_2 : person), % 4.74/4.99 Eq % 4.74/4.99 (∀ (GOVT : govt) (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.74/4.99 And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.99 (seatingEvent SE)) % 4.74/4.99 (performedBy SE a)) % 4.74/4.99 (seatedAtSide SE TS)) % 4.74/4.99 (govtRepresentedBy DE a_1 a)) % 4.74/4.99 (narrativeSuccessor CC a_1 GOVT)) % 4.74/4.99 (friendlyEvent VE)) % 4.74/4.99 (govtRepresentedBy VE GOVT a_2) → % 4.74/4.99 avoidTableSide a_2 VE TS) % 4.74/4.99 True % 4.74/4.99 Clause #135 (by clausification #[134]): ∀ (a : person) (a_1 a_2 : govt) (a_3 : person), % 4.74/4.99 Eq % 4.74/4.99 (∀ (CC : constrCont) (VE DE SE : event) (TS : table_side), % 4.74/4.99 And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.99 (seatingEvent SE)) % 4.74/4.99 (performedBy SE a)) % 4.74/4.99 (seatedAtSide SE TS)) % 4.74/4.99 (govtRepresentedBy DE a_1 a)) % 4.74/4.99 (narrativeSuccessor CC a_1 a_2)) % 4.74/4.99 (friendlyEvent VE)) % 4.74/4.99 (govtRepresentedBy VE a_2 a_3) → % 4.74/4.99 avoidTableSide a_3 VE TS) % 4.74/4.99 True % 4.74/4.99 Clause #136 (by clausification #[135]): ∀ (a : person) (a_1 : govt) (a_2 : constrCont) (a_3 : govt) (a_4 : person), % 4.74/4.99 Eq % 4.74/4.99 (∀ (VE DE SE : event) (TS : table_side), % 4.74/4.99 And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And % 4.74/4.99 (And (And (And (pastColocatedDiplomaticEvent VE DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/4.99 (seatingEvent SE)) % 4.74/4.99 (performedBy SE a)) % 4.74/4.99 (seatedAtSide SE TS)) % 4.74/4.99 (govtRepresentedBy DE a_1 a)) % 4.74/5.01 (narrativeSuccessor a_2 a_1 a_3)) % 4.74/5.01 (friendlyEvent VE)) % 4.74/5.01 (govtRepresentedBy VE a_3 a_4) → % 4.74/5.01 avoidTableSide a_4 VE TS) % 4.74/5.01 True % 4.74/5.01 Clause #137 (by clausification #[136]): ∀ (a : event) (a_1 : person) (a_2 : govt) (a_3 : constrCont) (a_4 : govt) (a_5 : person), % 4.74/5.01 Eq % 4.74/5.01 (∀ (DE SE : event) (TS : table_side), % 4.74/5.01 And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And (And (And (pastColocatedDiplomaticEvent a DE) (contentiousEvent DE)) (subEvents DE SE)) % 4.74/5.01 (seatingEvent SE)) % 4.74/5.01 (performedBy SE a_1)) % 4.74/5.01 (seatedAtSide SE TS)) % 4.74/5.01 (govtRepresentedBy DE a_2 a_1)) % 4.74/5.01 (narrativeSuccessor a_3 a_2 a_4)) % 4.74/5.01 (friendlyEvent a)) % 4.74/5.01 (govtRepresentedBy a a_4 a_5) → % 4.74/5.01 avoidTableSide a_5 a TS) % 4.74/5.01 True % 4.74/5.01 Clause #138 (by clausification #[137]): ∀ (a a_1 : event) (a_2 : person) (a_3 : govt) (a_4 : constrCont) (a_5 : govt) (a_6 : person), % 4.74/5.01 Eq % 4.74/5.01 (∀ (SE : event) (TS : table_side), % 4.74/5.01 And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 SE)) % 4.74/5.01 (seatingEvent SE)) % 4.74/5.01 (performedBy SE a_2)) % 4.74/5.01 (seatedAtSide SE TS)) % 4.74/5.01 (govtRepresentedBy a_1 a_3 a_2)) % 4.74/5.01 (narrativeSuccessor a_4 a_3 a_5)) % 4.74/5.01 (friendlyEvent a)) % 4.74/5.01 (govtRepresentedBy a a_5 a_6) → % 4.74/5.01 avoidTableSide a_6 a TS) % 4.74/5.01 True % 4.74/5.01 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), % 4.74/5.01 Eq % 4.74/5.01 (∀ (TS : table_side), % 4.74/5.01 And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.74/5.01 (seatingEvent a_2)) % 4.74/5.01 (performedBy a_2 a_3)) % 4.74/5.01 (seatedAtSide a_2 TS)) % 4.74/5.01 (govtRepresentedBy a_1 a_4 a_3)) % 4.74/5.01 (narrativeSuccessor a_5 a_4 a_6)) % 4.74/5.01 (friendlyEvent a)) % 4.74/5.01 (govtRepresentedBy a a_6 a_7) → % 4.74/5.01 avoidTableSide a_7 a TS) % 4.74/5.01 True % 4.74/5.01 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), % 4.74/5.01 Eq % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.74/5.01 (seatingEvent a_2)) % 4.74/5.01 (performedBy a_2 a_3)) % 4.74/5.01 (seatedAtSide a_2 a_4)) % 4.74/5.01 (govtRepresentedBy a_1 a_5 a_3)) % 4.74/5.01 (narrativeSuccessor a_6 a_5 a_7)) % 4.74/5.01 (friendlyEvent a)) % 4.74/5.01 (govtRepresentedBy a a_7 a_8) → % 4.74/5.01 avoidTableSide a_8 a a_4) % 4.74/5.01 True % 4.74/5.01 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), % 4.74/5.01 Or % 4.74/5.01 (Eq % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And (And (And (pastColocatedDiplomaticEvent a a_1) (contentiousEvent a_1)) (subEvents a_1 a_2)) % 4.74/5.01 (seatingEvent a_2)) % 4.74/5.01 (performedBy a_2 a_3)) % 4.74/5.01 (seatedAtSide a_2 a_4)) % 4.74/5.01 (govtRepresentedBy a_1 a_5 a_3)) % 4.74/5.01 (narrativeSuccessor a_6 a_5 a_7)) % 4.74/5.01 (friendlyEvent a)) % 4.74/5.01 (govtRepresentedBy a a_7 a_8)) % 4.74/5.01 False) % 4.74/5.01 (Eq (avoidTableSide a_8 a a_4) True) % 4.74/5.01 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) % 4.74/5.01 (a_8 : govt), % 4.74/5.01 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.01 (Or % 4.74/5.01 (Eq % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.01 (And % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_3) (contentiousEvent a_3)) (subEvents a_3 a_4)) % 4.74/5.02 (seatingEvent a_4)) % 4.74/5.02 (performedBy a_4 a_5)) % 4.74/5.02 (seatedAtSide a_4 a_2)) % 4.74/5.02 (govtRepresentedBy a_3 a_6 a_5)) % 4.74/5.02 (narrativeSuccessor a_7 a_6 a_8)) % 4.74/5.02 (friendlyEvent a_1)) % 4.74/5.02 False) % 4.74/5.02 (Eq (govtRepresentedBy a_1 a_8 a) False)) % 4.74/5.02 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) % 4.74/5.02 (a_8 : constrCont), % 4.74/5.02 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.74/5.02 (Or % 4.74/5.02 (Eq % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 4.74/5.02 (seatingEvent a_5)) % 4.74/5.02 (performedBy a_5 a_6)) % 4.74/5.02 (seatedAtSide a_5 a_2)) % 4.74/5.02 (govtRepresentedBy a_4 a_7 a_6)) % 4.74/5.02 (narrativeSuccessor a_8 a_7 a_3)) % 4.74/5.02 False) % 4.74/5.02 (Eq (friendlyEvent a_1) False))) % 4.74/5.02 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) % 4.74/5.02 (a_8 : constrCont), % 4.74/5.02 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.74/5.02 (Or (Eq (friendlyEvent a_1) False) % 4.74/5.02 (Or % 4.74/5.02 (Eq % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_4) (contentiousEvent a_4)) (subEvents a_4 a_5)) % 4.74/5.02 (seatingEvent a_5)) % 4.74/5.02 (performedBy a_5 a_6)) % 4.74/5.02 (seatedAtSide a_5 a_2)) % 4.74/5.02 (govtRepresentedBy a_4 a_7 a_6)) % 4.74/5.02 False) % 4.74/5.02 (Eq (narrativeSuccessor a_8 a_7 a_3) False)))) % 4.74/5.02 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) % 4.74/5.02 (a_8 : person), % 4.74/5.02 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.74/5.02 (Or (Eq (friendlyEvent a_1) False) % 4.74/5.02 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.74/5.02 (Or % 4.74/5.02 (Eq % 4.74/5.02 (And % 4.74/5.02 (And % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_7)) % 4.74/5.02 (seatingEvent a_7)) % 4.74/5.02 (performedBy a_7 a_8)) % 4.74/5.02 (seatedAtSide a_7 a_2)) % 4.74/5.02 False) % 4.74/5.02 (Eq (govtRepresentedBy a_6 a_5 a_8) False))))) % 4.74/5.02 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) % 4.74/5.02 (a_7 : person) (a_8 : event), % 4.74/5.02 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.74/5.02 (Or (Eq (friendlyEvent a_1) False) % 4.74/5.02 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.74/5.02 (Or % 4.74/5.02 (Eq % 4.74/5.02 (And % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.74/5.02 (seatingEvent a_8)) % 4.74/5.02 (performedBy a_8 a_7)) % 4.74/5.02 False) % 4.74/5.02 (Eq (seatedAtSide a_8 a_2) False)))))) % 4.74/5.02 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) % 4.74/5.02 (a_7 : person) (a_8 : event), % 4.74/5.02 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.74/5.02 (Or (Eq (friendlyEvent a_1) False) % 4.74/5.02 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.74/5.02 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.74/5.02 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.74/5.02 (Or % 4.74/5.02 (Eq % 4.74/5.02 (And (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.86/5.04 (seatingEvent a_8)) % 4.86/5.04 False) % 4.86/5.04 (Eq (performedBy a_8 a_7) False))))))) % 4.86/5.04 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) % 4.86/5.04 (a_7 : person) (a_8 : event), % 4.86/5.04 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.86/5.04 (Or (Eq (friendlyEvent a_1) False) % 4.86/5.04 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.86/5.04 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.86/5.04 (Or (Eq (performedBy a_8 a_7) False) % 4.86/5.04 (Or % 4.86/5.04 (Eq (And (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) (subEvents a_6 a_8)) % 4.86/5.04 False) % 4.86/5.04 (Eq (seatingEvent a_8) False)))))))) % 4.86/5.04 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) % 4.86/5.04 (a_7 : person) (a_8 : event), % 4.86/5.04 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.86/5.04 (Or (Eq (friendlyEvent a_1) False) % 4.86/5.04 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.86/5.04 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.86/5.04 (Or (Eq (performedBy a_8 a_7) False) % 4.86/5.04 (Or (Eq (seatingEvent a_8) False) % 4.86/5.04 (Or (Eq (And (pastColocatedDiplomaticEvent a_1 a_6) (contentiousEvent a_6)) False) % 4.86/5.04 (Eq (subEvents a_6 a_8) False))))))))) % 4.86/5.04 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) % 4.86/5.04 (a_7 : person) (a_8 : event), % 4.86/5.04 Or (Eq (avoidTableSide a a_1 a_2) True) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_1 a_3 a) False) % 4.86/5.04 (Or (Eq (friendlyEvent a_1) False) % 4.86/5.04 (Or (Eq (narrativeSuccessor a_4 a_5 a_3) False) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_6 a_5 a_7) False) % 4.86/5.04 (Or (Eq (seatedAtSide a_8 a_2) False) % 4.86/5.04 (Or (Eq (performedBy a_8 a_7) False) % 4.86/5.04 (Or (Eq (seatingEvent a_8) False) % 4.86/5.04 (Or (Eq (subEvents a_6 a_8) False) % 4.86/5.04 (Or (Eq (pastColocatedDiplomaticEvent a_1 a_6) False) (Eq (contentiousEvent a_6) False)))))))))) % 4.86/5.04 Clause #156 (by superposition #[150, 50]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.86/5.04 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.04 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 4.86/5.04 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.86/5.04 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.86/5.04 (Or (Eq (seatedAtSide a_5 a) False) % 4.86/5.04 (Or (Eq (performedBy a_5 a_4) False) % 4.86/5.04 (Or (Eq (seatingEvent a_5) False) % 4.86/5.04 (Or (Eq (subEvents a_3 a_5) False) % 4.86/5.04 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.86/5.04 (Or (Eq (contentiousEvent a_3) False) (Eq False True)))))))))) % 4.86/5.04 Clause #157 (by clausification #[131]): Eq (eventOccursAt compiegneVisit2018 france) True % 4.86/5.04 Clause #160 (by clausification #[85]): ∀ (a : event), Or (Eq (endsBeforeStartOf armistice1918 a) True) (Eq (endsBeforeStartOf armistice1940 a) False) % 4.86/5.04 Clause #161 (by superposition #[160, 52]): Or (Eq (endsBeforeStartOf armistice1918 compiegneVisit2018) True) (Eq False True) % 4.86/5.04 Clause #162 (by clausification #[161]): Eq (endsBeforeStartOf armistice1918 compiegneVisit2018) True % 4.86/5.04 Clause #164 (by superposition #[162, 119]): ∀ (a : geographicalRegion), % 4.86/5.04 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.04 (Or (Eq True False) % 4.86/5.04 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 4.86/5.04 (Or (Eq (diplomaticEvent armistice1918) False) (Eq (eventOccursAt armistice1918 a) False)))) % 4.86/5.04 Clause #167 (by clausification #[82]): ∀ (a : geographicalRegion), Or (Eq (subRegions france a) True) (Eq (subRegions hautsDeFrance a) False) % 4.86/5.04 Clause #173 (by clausification #[83]): ∀ (a : geographicalRegion), Or (Eq (subRegions hautsDeFrance a) True) (Eq (subRegions picardy a) False) % 4.86/5.06 Clause #174 (by superposition #[173, 7]): Or (Eq (subRegions hautsDeFrance rethondesCompiegne) True) (Eq False True) % 4.86/5.06 Clause #179 (by clausification #[174]): Eq (subRegions hautsDeFrance rethondesCompiegne) True % 4.86/5.06 Clause #182 (by superposition #[179, 167]): Or (Eq (subRegions france rethondesCompiegne) True) (Eq True False) % 4.86/5.06 Clause #184 (by clausification #[182]): Eq (subRegions france rethondesCompiegne) True % 4.86/5.06 Clause #191 (by clausification #[92]): ∀ (a : geographicalRegion), Or (Eq (eventOccursAt armistice1918 a) True) (Eq (subRegions a rethondesCompiegne) False) % 4.86/5.06 Clause #194 (by superposition #[191, 184]): Or (Eq (eventOccursAt armistice1918 france) True) (Eq False True) % 4.86/5.06 Clause #195 (by clausification #[194]): Eq (eventOccursAt armistice1918 france) True % 4.86/5.06 Clause #217 (by clausification #[102]): ∀ (a : govt), % 4.86/5.06 Or (Eq (narrativeSuccessor germania germanEmpire a) True) (Eq (narrativeSuccessor germania weimarRepublic a) False) % 4.86/5.06 Clause #218 (by superposition #[217, 12]): Or (Eq (narrativeSuccessor germania germanEmpire thirdReich) True) (Eq False True) % 4.86/5.06 Clause #219 (by clausification #[218]): Eq (narrativeSuccessor germania germanEmpire thirdReich) True % 4.86/5.06 Clause #220 (by superposition #[219, 99]): ∀ (a : govt), % 4.86/5.06 Or (Eq (narrativeSuccessor germania germanEmpire a) True) % 4.86/5.06 (Or (Eq True False) (Eq (narrativeSuccessor germania thirdReich a) False)) % 4.86/5.06 Clause #226 (by clausification #[103]): ∀ (a : govt), % 4.86/5.06 Or (Eq (narrativeSuccessor germania thirdReich a) True) % 4.86/5.06 (Eq (narrativeSuccessor germania alliedOccupiedGermany a) False) % 4.86/5.06 Clause #227 (by superposition #[226, 14]): Or (Eq (narrativeSuccessor germania thirdReich federalGermanRepublic) True) (Eq False True) % 4.86/5.06 Clause #228 (by clausification #[227]): Eq (narrativeSuccessor germania thirdReich federalGermanRepublic) True % 4.86/5.06 Clause #232 (by clausification #[220]): ∀ (a : govt), % 4.86/5.06 Or (Eq (narrativeSuccessor germania germanEmpire a) True) (Eq (narrativeSuccessor germania thirdReich a) False) % 4.86/5.06 Clause #234 (by superposition #[232, 228]): Or (Eq (narrativeSuccessor germania germanEmpire federalGermanRepublic) True) (Eq False True) % 4.86/5.06 Clause #235 (by clausification #[234]): Eq (narrativeSuccessor germania germanEmpire federalGermanRepublic) True % 4.86/5.06 Clause #259 (by clausification #[164]): ∀ (a : geographicalRegion), % 4.86/5.06 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.06 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) % 4.86/5.06 (Or (Eq (diplomaticEvent armistice1918) False) (Eq (eventOccursAt armistice1918 a) False))) % 4.86/5.06 Clause #260 (by forward demodulation #[259, 111]): ∀ (a : geographicalRegion), % 4.86/5.06 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.06 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Or (Eq True False) (Eq (eventOccursAt armistice1918 a) False))) % 4.86/5.06 Clause #261 (by clausification #[260]): ∀ (a : geographicalRegion), % 4.86/5.06 Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.06 (Or (Eq (eventOccursAt compiegneVisit2018 a) False) (Eq (eventOccursAt armistice1918 a) False)) % 4.86/5.06 Clause #265 (by superposition #[261, 157]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.06 (Or (Eq (eventOccursAt armistice1918 france) False) (Eq False True)) % 4.86/5.06 Clause #266 (by clausification #[265]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) % 4.86/5.06 (Eq (eventOccursAt armistice1918 france) False) % 4.86/5.06 Clause #267 (by forward demodulation #[266, 195]): Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True) (Eq True False) % 4.86/5.06 Clause #268 (by clausification #[267]): Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) True % 4.86/5.06 Clause #299 (by clausification #[156]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.86/5.06 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.06 (Or (Eq (friendlyEvent compiegneVisit2018) False) % 4.86/5.06 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.86/5.06 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.86/5.07 (Or (Eq (seatedAtSide a_5 a) False) % 4.86/5.07 (Or (Eq (performedBy a_5 a_4) False) % 4.86/5.07 (Or (Eq (seatingEvent a_5) False) % 4.86/5.07 (Or (Eq (subEvents a_3 a_5) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.86/5.07 (Eq (contentiousEvent a_3) False))))))))) % 4.86/5.07 Clause #300 (by forward demodulation #[299, 49]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq True False) % 4.86/5.07 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.86/5.07 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.86/5.07 (Or (Eq (seatedAtSide a_5 a) False) % 4.86/5.07 (Or (Eq (performedBy a_5 a_4) False) % 4.86/5.07 (Or (Eq (seatingEvent a_5) False) % 4.86/5.07 (Or (Eq (subEvents a_3 a_5) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.86/5.07 (Eq (contentiousEvent a_3) False))))))))) % 4.86/5.07 Clause #301 (by clausification #[300]): ∀ (a : table_side) (a_1 : constrCont) (a_2 : govt) (a_3 : event) (a_4 : person) (a_5 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (narrativeSuccessor a_1 a_2 federalGermanRepublic) False) % 4.86/5.07 (Or (Eq (govtRepresentedBy a_3 a_2 a_4) False) % 4.86/5.07 (Or (Eq (seatedAtSide a_5 a) False) % 4.86/5.07 (Or (Eq (performedBy a_5 a_4) False) % 4.86/5.07 (Or (Eq (seatingEvent a_5) False) % 4.86/5.07 (Or (Eq (subEvents a_3 a_5) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_3) False) % 4.86/5.07 (Eq (contentiousEvent a_3) False)))))))) % 4.86/5.07 Clause #304 (by superposition #[301, 235]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (govtRepresentedBy a_1 germanEmpire a_2) False) % 4.86/5.07 (Or (Eq (seatedAtSide a_3 a) False) % 4.86/5.07 (Or (Eq (performedBy a_3 a_2) False) % 4.86/5.07 (Or (Eq (seatingEvent a_3) False) % 4.86/5.07 (Or (Eq (subEvents a_1 a_3) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 4.86/5.07 (Or (Eq (contentiousEvent a_1) False) (Eq False True)))))))) % 4.86/5.07 Clause #307 (by clausification #[304]): ∀ (a : table_side) (a_1 : event) (a_2 : person) (a_3 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (govtRepresentedBy a_1 germanEmpire a_2) False) % 4.86/5.07 (Or (Eq (seatedAtSide a_3 a) False) % 4.86/5.07 (Or (Eq (performedBy a_3 a_2) False) % 4.86/5.07 (Or (Eq (seatingEvent a_3) False) % 4.86/5.07 (Or (Eq (subEvents a_1 a_3) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 a_1) False) % 4.86/5.07 (Eq (contentiousEvent a_1) False))))))) % 4.86/5.07 Clause #308 (by superposition #[307, 21]): ∀ (a : table_side) (a_1 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.07 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.07 (Or (Eq (seatingEvent a_1) False) % 4.86/5.07 (Or (Eq (subEvents armistice1918 a_1) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) False) % 4.86/5.07 (Or (Eq (contentiousEvent armistice1918) False) (Eq False True))))))) % 4.86/5.07 Clause #309 (by clausification #[308]): ∀ (a : table_side) (a_1 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.07 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.07 (Or (Eq (seatingEvent a_1) False) % 4.86/5.07 (Or (Eq (subEvents armistice1918 a_1) False) % 4.86/5.07 (Or (Eq (pastColocatedDiplomaticEvent compiegneVisit2018 armistice1918) False) % 4.86/5.07 (Eq (contentiousEvent armistice1918) False)))))) % 4.86/5.07 Clause #310 (by forward demodulation #[309, 268]): ∀ (a : table_side) (a_1 : event), % 4.86/5.07 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.07 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.07 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.07 (Or (Eq (seatingEvent a_1) False) % 4.86/5.07 (Or (Eq (subEvents armistice1918 a_1) False) % 4.86/5.08 (Or (Eq True False) (Eq (contentiousEvent armistice1918) False)))))) % 4.86/5.08 Clause #311 (by clausification #[310]): ∀ (a : table_side) (a_1 : event), % 4.86/5.08 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.08 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.08 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.08 (Or (Eq (seatingEvent a_1) False) % 4.86/5.08 (Or (Eq (subEvents armistice1918 a_1) False) (Eq (contentiousEvent armistice1918) False))))) % 4.86/5.08 Clause #312 (by forward demodulation #[311, 107]): ∀ (a : table_side) (a_1 : event), % 4.86/5.08 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.08 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.08 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.08 (Or (Eq (seatingEvent a_1) False) (Or (Eq (subEvents armistice1918 a_1) False) (Eq True False))))) % 4.86/5.08 Clause #313 (by clausification #[312]): ∀ (a : table_side) (a_1 : event), % 4.86/5.08 Or (Eq (avoidTableSide merkel compiegneVisit2018 a) True) % 4.86/5.08 (Or (Eq (seatedAtSide a_1 a) False) % 4.86/5.08 (Or (Eq (performedBy a_1 erzberger) False) % 4.86/5.08 (Or (Eq (seatingEvent a_1) False) (Eq (subEvents armistice1918 a_1) False)))) % 4.86/5.08 Clause #314 (by superposition #[313, 30]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Or (Eq (performedBy armistice1918GermanSeating erzberger) False) % 4.86/5.08 (Or (Eq (seatingEvent armistice1918GermanSeating) False) % 4.86/5.08 (Or (Eq (subEvents armistice1918 armistice1918GermanSeating) False) (Eq False True)))) % 4.86/5.08 Clause #330 (by clausification #[314]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Or (Eq (performedBy armistice1918GermanSeating erzberger) False) % 4.86/5.08 (Or (Eq (seatingEvent armistice1918GermanSeating) False) % 4.86/5.08 (Eq (subEvents armistice1918 armistice1918GermanSeating) False))) % 4.86/5.08 Clause #331 (by forward demodulation #[330, 29]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Or (Eq True False) % 4.86/5.08 (Or (Eq (seatingEvent armistice1918GermanSeating) False) % 4.86/5.08 (Eq (subEvents armistice1918 armistice1918GermanSeating) False))) % 4.86/5.08 Clause #332 (by clausification #[331]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Or (Eq (seatingEvent armistice1918GermanSeating) False) % 4.86/5.08 (Eq (subEvents armistice1918 armistice1918GermanSeating) False)) % 4.86/5.08 Clause #333 (by forward demodulation #[332, 27]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Or (Eq True False) (Eq (subEvents armistice1918 armistice1918GermanSeating) False)) % 4.86/5.08 Clause #334 (by clausification #[333]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) % 4.86/5.08 (Eq (subEvents armistice1918 armistice1918GermanSeating) False) % 4.86/5.08 Clause #335 (by forward demodulation #[334, 28]): Or (Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True) (Eq True False) % 4.86/5.08 Clause #336 (by clausification #[335]): Eq (avoidTableSide merkel compiegneVisit2018 cwlTableSideC) True % 4.86/5.08 Clause #337 (by superposition #[336, 112]): Eq True False % 4.86/5.08 Clause #338 (by clausification #[337]): False % 4.86/5.08 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------