Erin is green. Erin is nice. Erin is rough. Rough things are blue. All blue things are quiet. All nice, blue things are cold. All nice things are quiet. If something is quiet and white then it is green. All quiet things are rough.
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
All nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and white then it is green.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Erin is rough.
True
1
proof
[(triple3 OR ((((triple2) -> rule4)) -> rule6))]
("Erin" "is" "rough" "+")
triple3
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple3 OR ((((triple2) -> rule4)) -> rule6))]
("Erin" "is" "rough" "-")
triple3
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is quiet.
True
2
proof
[(((triple2) -> rule4) OR ((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3) -> rule1)) -> rule2))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
True
4
proof
[(((triple2 ((triple3) -> rule1)) -> rule3) OR ((triple2 ((((((triple2) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
("Erin" "is" "cold" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is not cold.
False
4
inv-proof
[(((triple2 ((triple3) -> rule1)) -> rule3) OR ((triple2 ((((((triple2) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
("Erin" "is" "cold" "-")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
@0: Erin is green.[(triple1)] Erin is nice.[(triple2)] Erin is rough.[(triple3 OR ((((triple2) -> rule4)) -> rule6))] @1: Erin is blue.[(((triple3) -> rule1) OR ((((((triple2) -> rule4)) -> rule6)) -> rule1))] Erin is quiet.[(((triple2) -> rule4) OR ((((triple3) -> rule1)) -> rule2))] @2: Erin is cold.[(((triple2 ((triple3) -> rule1)) -> rule3) OR ((triple2 ((((((triple2) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4