Bob is big. Bob is cold. Bob is nice. Bob is quiet. Erin is big. Erin is nice. Erin is quiet. Nice, furry things are cold. Quiet, nice things are white. If something is cold then it is rough. If Erin is white then Erin is big. If Bob is cold then Bob is rough. If something is big then it is furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Nice, furry things are cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Quiet, nice things are white.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Erin is white then Erin is big.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "big" "+"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Erin is not quiet.
False
1
inv-proof
[(triple7)]
("Erin" "is" "quiet" "-")
triple7
Bob is white.
True
3
proof
[(((triple4 triple3) -> rule2))]
("Bob" "is" "white" "+")
((triple4 triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
3
inv-proof
[(((triple4 triple3) -> rule2))]
("Bob" "is" "white" "-")
((triple4 triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is cold.
True
4
proof
[(((triple6 ((triple5) -> rule6)) -> rule1) OR ((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1))]
("Erin" "is" "cold" "+")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple6 ((((((triple7 triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is not cold.
False
4
inv-proof
[(((triple6 ((triple5) -> rule6)) -> rule1) OR ((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1))]
("Erin" "is" "cold" "-")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple6 ((((((triple7 triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is rough.
True
5
proof
[(((((triple6 ((triple5) -> rule6)) -> rule1)) -> rule3) OR ((((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
("Erin" "is" "rough" "+")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple6 ((((((triple7 triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
Erin is not rough.
False
5
inv-proof
[(((((triple6 ((triple5) -> rule6)) -> rule1)) -> rule3) OR ((((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
("Erin" "is" "rough" "-")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple6 ((((((triple7 triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple3 ((triple1) -> rule6)) -> rule1))] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Erin is big.[(triple5 OR ((((triple7 triple6) -> rule2)) -> rule4))] Erin is nice.[(triple6)] Erin is quiet.[(triple7)] @1: Bob is furry.[(((triple1) -> rule6))] Bob is rough.[(((triple2) -> rule3) OR ((triple2) -> rule5) OR ((((triple3 ((triple1) -> rule6)) -> rule1)) -> rule3) OR ((((triple3 ((triple1) -> rule6)) -> rule1)) -> rule5))] Bob is white.[(((triple4 triple3) -> rule2))] Erin is furry.[(((triple5) -> rule6) OR ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6))] Erin is white.[(((triple7 triple6) -> rule2))] @2: Erin is cold.[(((triple6 ((triple5) -> rule6)) -> rule1) OR ((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1))] @3: Erin is rough.[(((((triple6 ((triple5) -> rule6)) -> rule1)) -> rule3) OR ((((triple6 ((((((triple7 triple6) -> rule2)) -> rule4)) -> rule6)) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((((triple7 triple6) -> (rule2 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple2) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple3 ((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple3 ((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple4 triple3) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple5) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((((triple7 triple6) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple7 triple6) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple6 ((((((triple7 triple6) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple6 ((((((triple7 triple6) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
int5