Bob is blue. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is red. Bob is white. Erin is blue. Erin is cold. Erin is furry. Erin is kind. Erin is red. Blue, furry people are red. Furry, green people are white. All blue, cold people are green. Blue, cold people are red. If Bob is cold and Bob is blue then Bob is furry. All blue people are furry. All blue people are cold. All blue people are red.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Blue, furry people are red.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Furry, green people are white.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All blue, cold people are green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Blue, cold people are red.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If Bob is cold and Bob is blue then Bob is furry.
((("Bob" "is" "cold" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "furry" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Bob is cold.
True
1
proof
[(triple2 OR ((triple1) -> rule7))]
("Bob" "is" "cold" "+")
triple2
((triple1) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not white.
False
1
inv-proof
[(triple7 OR ((triple3 triple4) -> rule2) OR ((triple3 ((triple1 triple2) -> rule3)) -> rule2) OR ((((triple1) -> rule6) triple4) -> rule2) OR ((((triple2 triple1) -> rule5) triple4) -> rule2) OR ((((triple1) -> rule6) ((triple1 triple2) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule5) ((triple1 triple2) -> rule3)) -> rule2) OR ((triple3 ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) triple4) -> rule2) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule5) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) ((triple1 triple2) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2))]
("Bob" "is" "white" "-")
triple7
((triple3 triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple2 triple1) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple2 triple1) -> (rule5 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple3 ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int4)) ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((triple2 triple1) -> (rule5 % int4)) ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((triple1) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((((triple1) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple1) -> rule7))] Bob is furry.[(triple3 OR ((triple1) -> rule6) OR ((triple2 triple1) -> rule5) OR ((((triple1) -> rule7) triple1) -> rule5))] Bob is green.[(triple4 OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple1) -> rule7)) -> rule3))] Bob is kind.[(triple5)] Bob is red.[(triple6 OR ((triple1) -> rule8) OR ((triple1 triple2) -> rule4) OR ((triple1 triple3) -> rule1) OR ((triple1 ((triple1) -> rule6)) -> rule1) OR ((triple1 ((triple1) -> rule7)) -> rule4) OR ((triple1 ((triple2 triple1) -> rule5)) -> rule1) OR ((triple1 ((((triple1) -> rule7) triple1) -> rule5)) -> rule1))] Bob is white.[(triple7 OR ((triple3 triple4) -> rule2) OR ((triple3 ((triple1 triple2) -> rule3)) -> rule2) OR ((((triple1) -> rule6) triple4) -> rule2) OR ((((triple2 triple1) -> rule5) triple4) -> rule2) OR ((((triple1) -> rule6) ((triple1 triple2) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule5) ((triple1 triple2) -> rule3)) -> rule2) OR ((triple3 ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) triple4) -> rule2) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((triple2 triple1) -> rule5) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) ((triple1 triple2) -> rule3)) -> rule2) OR ((((((triple1) -> rule7) triple1) -> rule5) ((triple1 ((triple1) -> rule7)) -> rule3)) -> rule2))] Erin is blue.[(triple8)] Erin is cold.[(triple9 OR ((triple8) -> rule7))] Erin is furry.[(triple10 OR ((triple8) -> rule6))] Erin is kind.[(triple11)] Erin is red.[(triple12 OR ((triple8) -> rule8) OR ((triple8 triple10) -> rule1) OR ((triple8 triple9) -> rule4) OR ((triple8 ((triple8) -> rule6)) -> rule1) OR ((triple8 ((triple8) -> rule7)) -> rule4))] @1: Erin is green.[(((triple8 triple9) -> rule3) OR ((triple8 ((triple8) -> rule7)) -> rule3))] @2: Erin is white.[(((triple10 ((triple8 triple9) -> rule3)) -> rule2) OR ((((triple8) -> rule6) ((triple8 triple9) -> rule3)) -> rule2) OR ((triple10 ((triple8 ((triple8) -> rule7)) -> rule3)) -> rule2) OR ((((triple8) -> rule6) ((triple8 ((triple8) -> rule7)) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple2 triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple1 triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1 ((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 triple2) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 triple3) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple1 ((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple1 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple1 ((((triple1) -> (rule7 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple3 triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple2 triple1) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple2 triple1) -> (rule5 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple3 ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int4)) ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((triple2 triple1) -> (rule5 % int4)) ((triple1 ((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((triple1) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((triple1 triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
((((((triple1) -> (rule7 % int4)) triple1) -> (rule5 % int3)) ((triple1 ((triple1) -> (rule7 % int4))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is cold.
("Erin" "is" "cold" "+")
triple9
((triple8) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple8) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
((triple8) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 triple9) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((triple8 ((triple8) -> (rule7 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple8 triple9) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple8 ((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple10 ((triple8 triple9) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple8) -> (rule6 % int3)) ((triple8 triple9) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((triple10 ((triple8 ((triple8) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((triple8) -> (rule6 % int4)) ((triple8 ((triple8) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4