Bob is blue. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is red. Bob is round. Charlie is furry. Charlie is green. Charlie is kind. Charlie is red. Charlie is round. All green things are round. Blue things are cold. Red things are cold. If Bob is blue and Bob is cold then Bob is furry. Kind, red things are green. Cold things are furry. All round, blue things are kind. All kind things are furry.
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 round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If Bob is blue and Bob is cold then Bob is furry.
((("Bob" "is" "blue" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "furry" "+"))
Kind, red things are green.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All round, blue things are kind.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Bob is furry.
True
1
proof
[(triple3 OR ((triple2) -> rule6) OR ((triple5) -> rule8) OR ((triple1 triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule6) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple7 triple1) -> rule7)) -> rule8) OR ((triple1 ((triple1) -> rule2)) -> rule4) OR ((triple1 ((triple6) -> rule3)) -> rule4) OR ((((((triple4) -> rule1) triple1) -> rule7)) -> rule8))]
("Bob" "is" "furry" "+")
triple3
((triple2) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple7 triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple1 ((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple4) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Charlie is not round.
False
1
inv-proof
[(triple12 OR ((triple9) -> rule1) OR ((((triple10 triple11) -> rule5)) -> rule1))]
("Charlie" "is" "round" "-")
triple12
((triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple10 triple11) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple1) -> rule2) OR ((triple6) -> rule3))] Bob is furry.[(triple3 OR ((triple2) -> rule6) OR ((triple5) -> rule8) OR ((triple1 triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule6) OR ((((triple6) -> rule3)) -> rule6) OR ((((triple7 triple1) -> rule7)) -> rule8) OR ((triple1 ((triple1) -> rule2)) -> rule4) OR ((triple1 ((triple6) -> rule3)) -> rule4) OR ((((((triple4) -> rule1) triple1) -> rule7)) -> rule8))] Bob is green.[(triple4 OR ((triple5 triple6) -> rule5) OR ((((triple7 triple1) -> rule7) triple6) -> rule5))] Bob is kind.[(triple5 OR ((triple7 triple1) -> rule7) OR ((((triple4) -> rule1) triple1) -> rule7))] Bob is red.[(triple6)] Bob is round.[(triple7 OR ((triple4) -> rule1) OR ((((triple5 triple6) -> rule5)) -> rule1))] Charlie is furry.[(triple8 OR ((triple10) -> rule8) OR ((((triple11) -> rule3)) -> rule6))] Charlie is green.[(triple9 OR ((triple10 triple11) -> rule5))] Charlie is kind.[(triple10)] Charlie is red.[(triple11)] Charlie is round.[(triple12 OR ((triple9) -> rule1) OR ((((triple10 triple11) -> rule5)) -> rule1))] @1: Charlie is cold.[(((triple11) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple2) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple1 triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple7 triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((triple1 ((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((((triple4) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple4
((triple5 triple6) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple7 triple1) -> (rule7 % int2)) triple6) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple7 triple1) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple4) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
((triple4) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple5 triple6) -> (rule5 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
((triple10) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple11) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple10 triple11) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
((triple9) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple10 triple11) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple11) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1