Erin is cold. Erin is kind. Erin is quiet. Erin is rough. Erin is round. Erin is white. Erin is young. If something is cold then it is kind. All quiet, young things are round. Kind things are cold. If Erin is young and Erin is kind then Erin is white. If something is quiet and white then it is cold. If something is rough and cold then it is white. If something is kind and quiet then it is rough. Rough, kind things are round.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All quiet, young things are round.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Erin is young and Erin is kind then Erin is white.
((("Erin" "is" "young" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "white" "+"))
If something is quiet and white then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is rough and cold then it is white.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is kind and quiet then it is rough.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Erin is rough.
True
1
proof
[(triple4 OR ((triple2 triple3) -> rule7) OR ((((triple1) -> rule1) triple3) -> rule7) OR ((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7))]
("Erin" "is" "rough" "+")
triple4
((triple2 triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not round.
False
1
inv-proof
[(triple5 OR ((triple3 triple7) -> rule2) OR ((triple4 triple2) -> rule8) OR ((triple4 ((triple1) -> rule1)) -> rule8) OR ((((triple2 triple3) -> rule7) triple2) -> rule8) OR ((((triple2 triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((triple4 ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) triple2) -> rule8) OR ((((triple2 triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) triple2) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8))]
("Erin" "is" "round" "-")
triple5
((triple3 triple7) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple2 triple3) -> (rule7 % int3)) ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple4 ((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple2 triple3) -> (rule7 % int4)) ((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3)) ((((triple3 triple6) -> (rule5 % int2))) -> (rule1 % int4))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
@0: Erin is cold.[(triple1 OR ((triple2) -> rule3) OR ((triple3 triple6) -> rule5) OR ((triple3 ((triple7 triple2) -> rule4)) -> rule5))] Erin is kind.[(triple2 OR ((triple1) -> rule1) OR ((((triple3 triple6) -> rule5)) -> rule1))] Erin is quiet.[(triple3)] Erin is rough.[(triple4 OR ((triple2 triple3) -> rule7) OR ((((triple1) -> rule1) triple3) -> rule7) OR ((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7))] Erin is round.[(triple5 OR ((triple3 triple7) -> rule2) OR ((triple4 triple2) -> rule8) OR ((triple4 ((triple1) -> rule1)) -> rule8) OR ((((triple2 triple3) -> rule7) triple2) -> rule8) OR ((((triple2 triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((triple4 ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) triple2) -> rule8) OR ((((triple2 triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((((((triple1) -> rule1) triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) triple2) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) ((triple1) -> rule1)) -> rule8) OR ((((((((triple3 triple6) -> rule5)) -> rule1) triple3) -> rule7) ((((triple3 triple6) -> rule5)) -> rule1)) -> rule8))] Erin is white.[(triple6 OR ((triple4 triple1) -> rule6) OR ((triple7 triple2) -> rule4) OR ((triple4 ((triple2) -> rule3)) -> rule6) OR ((triple7 ((triple1) -> rule1)) -> rule4) OR ((((triple2 triple3) -> rule7) triple1) -> rule6) OR ((((triple2 triple3) -> rule7) ((triple2) -> rule3)) -> rule6) OR ((((((triple1) -> rule1) triple3) -> rule7) triple1) -> rule6) OR ((((((triple1) -> rule1) triple3) -> rule7) ((triple2) -> rule3)) -> rule6))] Erin is young.[(triple7)]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
((triple2) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3 triple6) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple3 ((triple7 triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((triple3 triple6) -> (rule5 % int2))) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
((triple2 triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple3 triple7) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple2 triple3) -> (rule7 % int3)) ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple4 ((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple2 triple3) -> (rule7 % int4)) ((((triple3 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3)) ((((triple3 triple6) -> (rule5 % int2))) -> (rule1 % int4))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
((((((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3)) triple3) -> (rule7 % int2)) ((((triple3 triple6) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple4 triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple7 triple2) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple7 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple2 triple3) -> (rule7 % int3)) ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3)) ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
triple7