Erin is cold. Erin is green. Erin is red. Erin is rough. Erin is round. Erin is white. Erin is young. Green people are white. White, red people are young. If Erin is young then Erin is rough.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
White, red people are young.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If Erin is young then Erin is rough.
((("Erin" "is" "young" "+")) -> ("Erin" "is" "rough" "+"))
Erin is young.
True
1
proof
[(triple7 OR ((triple6 triple3) -> rule2) OR ((((triple2) -> rule1) triple3) -> rule2))]
("Erin" "is" "young" "+")
triple7
((triple6 triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule3) OR ((((triple6 triple3) -> rule2)) -> rule3) OR ((((((triple2) -> rule1) triple3) -> rule2)) -> rule3))]
("Erin" "is" "rough" "-")
triple4
((triple7) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple2) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
@0: Erin is cold.[(triple1)] Erin is green.[(triple2)] Erin is red.[(triple3)] Erin is rough.[(triple4 OR ((triple7) -> rule3) OR ((((triple6 triple3) -> rule2)) -> rule3) OR ((((((triple2) -> rule1) triple3) -> rule2)) -> rule3))] Erin is round.[(triple5)] Erin is white.[(triple6 OR ((triple2) -> rule1))] Erin is young.[(triple7 OR ((triple6 triple3) -> rule2) OR ((((triple2) -> rule1) triple3) -> rule2))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
((triple7) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((((triple2) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple2) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6 triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2