Bob is big. Bob is cold. Bob is furry. Bob is green. Bob is red. Bob is white. Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. If Bob is blue and Bob is furry then Bob is cold. Cold people are red. If someone is red and blue then they are green. All furry people are white. Red, big people are green. If someone is white then they are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
If Bob is blue and Bob is furry then Bob is cold.
((("Bob" "is" "blue" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "cold" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is red and blue then they are green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Red, big people are green.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Charlie is blue.
True
1
proof
[(triple8)]
("Charlie" "is" "blue" "+")
triple8
Bob is not green.
False
1
inv-proof
[(triple4 OR ((triple5 triple1) -> rule5) OR ((((triple2) -> rule2) triple1) -> rule5) OR ((((((triple6) -> rule6)) -> rule2) triple1) -> rule5) OR ((((((((triple3) -> rule4)) -> rule6)) -> rule2) triple1) -> rule5))]
("Bob" "is" "green" "-")
triple4
((triple5 triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple2) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Charlie is white.
True
2
proof
[(((triple9) -> rule4))]
("Charlie" "is" "white" "+")
((triple9) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple9) -> rule4))]
("Charlie" "is" "white" "-")
((triple9) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple9) -> rule4)) -> rule6))]
("Charlie" "is" "cold" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule6))]
("Charlie" "is" "cold" "-")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
True
4
proof
[(((((((triple9) -> rule4)) -> rule6)) -> rule2))]
("Charlie" "is" "red" "+")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not red.
False
4
inv-proof
[(((((((triple9) -> rule4)) -> rule6)) -> rule2))]
("Charlie" "is" "red" "-")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((triple6) -> rule6) OR ((((triple3) -> rule4)) -> rule6))] Bob is furry.[(triple3)] Bob is green.[(triple4 OR ((triple5 triple1) -> rule5) OR ((((triple2) -> rule2) triple1) -> rule5) OR ((((((triple6) -> rule6)) -> rule2) triple1) -> rule5) OR ((((((((triple3) -> rule4)) -> rule6)) -> rule2) triple1) -> rule5))] Bob is red.[(triple5 OR ((triple2) -> rule2) OR ((((triple6) -> rule6)) -> rule2) OR ((((((triple3) -> rule4)) -> rule6)) -> rule2))] Bob is white.[(triple6 OR ((triple3) -> rule4))] Charlie is big.[(triple7)] Charlie is blue.[(triple8)] Charlie is furry.[(triple9)] Charlie is green.[(triple10 OR ((((((((triple9) -> rule4)) -> rule6)) -> rule2) triple7) -> rule5) OR ((((((((triple9) -> rule4)) -> rule6)) -> rule2) triple8) -> rule3))] @1: Charlie is white.[(((triple9) -> rule4))] @2: Charlie is cold.[(((((triple9) -> rule4)) -> rule6))] @3: Charlie is red.[(((((((triple9) -> rule4)) -> rule6)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple5 triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple2) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
((((((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((((triple9) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is white.
("Charlie" "is" "white" "+")
((triple9) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3