Bob is not blue. Bob is cold. Bob is furry. Bob is green. Bob is kind. Bob is smart. Bob is young. Gary is blue. Gary is cold. Gary is furry. Gary is green. Gary is kind. Gary is smart. Gary is young. If something is green then it is cold. If something is green and not young then it is cold. If Gary is kind and Gary is green then Gary is cold. Furry things are kind. If something is green and not young then it is kind. If Bob is young then Bob is furry. If something is green and not cold then it is smart. If something is furry then it is smart.
Bob is not 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 smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is green and not young then it is cold.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "+"))
If Gary is kind and Gary is green then Gary is cold.
((("Gary" "is" "kind" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "cold" "+"))
Furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is green and not young then it is kind.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
If Bob is young then Bob is furry.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "furry" "+"))
If something is green and not cold then it is smart.
((("something" "is" "green" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Gary is green.
True
1
proof
[(triple11)]
("Gary" "is" "green" "+")
triple11
Gary is not cold.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule1) OR ((triple12 triple11) -> rule3) OR ((((triple10) -> rule4) triple11) -> rule3))]
("Gary" "is" "cold" "-")
triple9
((triple11) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple12 triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple10) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
@0: Bob is cold.[(triple2 OR ((triple4) -> rule1))] Bob is furry.[(triple3 OR ((triple7) -> rule6))] Bob is green.[(triple4)] Bob is kind.[(triple5 OR ((triple3) -> rule4) OR ((((triple7) -> rule6)) -> rule4))] Bob is not blue.[(triple1)] Bob is smart.[(triple6 OR ((triple3) -> rule8) OR ((((triple7) -> rule6)) -> rule8))] Bob is young.[(triple7)] Gary is blue.[(triple8)] Gary is cold.[(triple9 OR ((triple11) -> rule1) OR ((triple12 triple11) -> rule3) OR ((((triple10) -> rule4) triple11) -> rule3))] Gary is furry.[(triple10)] Gary is green.[(triple11)] Gary is kind.[(triple12 OR ((triple10) -> rule4))] Gary is smart.[(triple13 OR ((triple10) -> rule8))] Gary is young.[(triple14)]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple7) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple3) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
((triple11) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((triple12 triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple10) -> (rule4 % int2)) triple11) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
((triple10) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((triple10) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple14