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