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