Bob is big. Bob is blue. Bob is cold. Bob is kind. Bob is round. Bob is smart. Bob is young. Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is round. Gary is smart. Gary is young. Cold things are blue. If Bob is smart then Bob is round. All cold, blue things are round. If something is smart then it is blue. If something is cold and round then it is smart. If something is round and kind then it is smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If Bob is smart then Bob is round.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "round" "+"))
All cold, blue things are round.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is cold and round then it is smart.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is round and kind then it is smart.
((("something" "is" "round" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Gary is big.
True
1
proof
[(triple8)]
("Gary" "is" "big" "+")
triple8
Gary is not kind.
False
1
inv-proof
[(triple11)]
("Gary" "is" "kind" "-")
triple11
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple3) -> rule1) OR ((triple6) -> rule4) OR ((((triple3 triple5) -> rule5)) -> rule4) OR ((((triple5 triple4) -> rule6)) -> rule4))] Bob is cold.[(triple3)] Bob is kind.[(triple4)] Bob is round.[(triple5 OR ((triple6) -> rule2) OR ((triple3 triple2) -> rule3) OR ((triple3 ((triple3) -> rule1)) -> rule3) OR ((triple3 ((triple6) -> rule4)) -> rule3))] Bob is smart.[(triple6 OR ((triple3 triple5) -> rule5) OR ((triple5 triple4) -> rule6) OR ((triple3 ((triple3 triple2) -> rule3)) -> rule5) OR ((((triple3 triple2) -> rule3) triple4) -> rule6) OR ((triple3 ((triple3 ((triple3) -> rule1)) -> rule3)) -> rule5) OR ((((triple3 ((triple3) -> rule1)) -> rule3) triple4) -> rule6))] Bob is young.[(triple7)] Gary is big.[(triple8)] Gary is blue.[(triple9 OR ((triple10) -> rule1) OR ((triple13) -> rule4) OR ((((triple10 triple12) -> rule5)) -> rule4) OR ((((triple12 triple11) -> rule6)) -> rule4))] Gary is cold.[(triple10)] Gary is kind.[(triple11)] Gary is round.[(triple12 OR ((triple10 triple9) -> rule3) OR ((triple10 ((triple10) -> rule1)) -> rule3) OR ((triple10 ((triple13) -> rule4)) -> rule3))] Gary is smart.[(triple13 OR ((triple10 triple12) -> rule5) OR ((triple12 triple11) -> rule6) OR ((triple10 ((triple10 triple9) -> rule3)) -> rule5) OR ((((triple10 triple9) -> rule3) triple11) -> rule6) OR ((triple10 ((triple10 ((triple10) -> rule1)) -> rule3)) -> rule5) OR ((((triple10 ((triple10) -> rule1)) -> rule3) triple11) -> rule6))] Gary is young.[(triple14)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple6) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5 triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple6) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple3 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3 triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5 triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 ((triple3 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple3 triple2) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((triple3 ((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple10) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple13) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple10 triple12) -> (rule5 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple12 triple11) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple10 triple9) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple10 ((triple13) -> (rule4 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((triple10 triple12) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple12 triple11) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple10 ((triple10 triple9) -> (rule3 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple10 triple9) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((triple10 ((triple10 ((triple10) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((((triple10 ((triple10) -> (rule1 % int3))) -> (rule3 % int2)) triple11) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
triple14