Anne is big. Anne is red. Anne is white. Bob is big. Bob is blue. Bob is nice. Bob is red. Bob is rough. Bob is smart. Bob is white. Erin is big. Erin is blue. Erin is nice. Erin is rough. Erin is smart. Erin is white. If something is red and rough then it is smart. All white, big things are rough. If Anne is blue and Anne is big then Anne is white. Big, rough things are nice. If Erin is big and Erin is smart then Erin is nice. All white, big things are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is red and rough then it is smart.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
All white, big things are rough.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If Anne is blue and Anne is big then Anne is white.
((("Anne" "is" "blue" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "white" "+"))
Big, rough things are nice.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If Erin is big and Erin is smart then Erin is nice.
((("Erin" "is" "big" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "nice" "+"))
All white, big things are blue.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple10)]
("Bob" "is" "white" "+")
triple10
Erin is not big.
False
1
inv-proof
[(triple11)]
("Erin" "is" "big" "-")
triple11
Anne is rough.
True
3
proof
[(((triple3 triple1) -> rule2))]
("Anne" "is" "rough" "+")
((triple3 triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not blue.
False
3
inv-proof
[(((triple3 triple1) -> rule6))]
("Anne" "is" "blue" "-")
((triple3 triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
True
5
proof
[(((triple2 ((triple3 triple1) -> rule2)) -> rule1))]
("Anne" "is" "smart" "+")
((triple2 ((triple3 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not smart.
False
5
inv-proof
[(((triple2 ((triple3 triple1) -> rule2)) -> rule1))]
("Anne" "is" "smart" "-")
((triple2 ((triple3 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
@0: Anne is big.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3)] Bob is big.[(triple4)] Bob is blue.[(triple5 OR ((triple10 triple4) -> rule6))] Bob is nice.[(triple6 OR ((triple4 triple8) -> rule4) OR ((triple4 ((triple10 triple4) -> rule2)) -> rule4))] Bob is red.[(triple7)] Bob is rough.[(triple8 OR ((triple10 triple4) -> rule2))] Bob is smart.[(triple9 OR ((triple7 triple8) -> rule1) OR ((triple7 ((triple10 triple4) -> rule2)) -> rule1))] Bob is white.[(triple10)] Erin is big.[(triple11)] Erin is blue.[(triple12 OR ((triple16 triple11) -> rule6))] Erin is nice.[(triple13 OR ((triple11 triple14) -> rule4) OR ((triple11 triple15) -> rule5) OR ((triple11 ((triple16 triple11) -> rule2)) -> rule4))] Erin is rough.[(triple14 OR ((triple16 triple11) -> rule2))] Erin is smart.[(triple15)] Erin is white.[(triple16)] @1: Anne is blue.[(((triple3 triple1) -> rule6))] Anne is rough.[(((triple3 triple1) -> rule2))] @2: Anne is nice.[(((triple1 ((triple3 triple1) -> rule2)) -> rule4))] Anne is smart.[(((triple2 ((triple3 triple1) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
((triple10 triple4) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple6
((triple4 triple8) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple4 ((triple10 triple4) -> (rule2 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
triple8
((triple10 triple4) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple9
((triple7 triple8) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple7 ((triple10 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
Erin is blue.
("Erin" "is" "blue" "+")
triple12
((triple16 triple11) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple13
((triple11 triple14) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple11 triple15) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple11 ((triple16 triple11) -> (rule2 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple14
((triple16 triple11) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple15
Erin is white.
("Erin" "is" "white" "+")
triple16
Anne is blue.
("Anne" "is" "blue" "+")
((triple3 triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1 ((triple3 triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 ((triple3 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2