Bob is blue. Bob is cold. Bob is quiet. Bob is red. Bob is round. Bob is white. Bob is young. Gary is blue. Gary is cold. Gary is quiet. Gary is red. Gary is round. Gary is white. Gary is young. If someone is quiet and round then they are red. If someone is round and quiet then they are blue. Blue people are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is quiet and round then they are red.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is round and quiet then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Gary is white.
True
1
proof
[(triple13)]
("Gary" "is" "white" "+")
triple13
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
@0: Bob is blue.[(triple1 OR ((triple5 triple3) -> rule2))] Bob is cold.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple3 triple5) -> rule1))] Bob is round.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple1) -> rule3) OR ((((triple5 triple3) -> rule2)) -> rule3))] Gary is blue.[(triple8 OR ((triple12 triple10) -> rule2))] Gary is cold.[(triple9)] Gary is quiet.[(triple10)] Gary is red.[(triple11 OR ((triple10 triple12) -> rule1))] Gary is round.[(triple12)] Gary is white.[(triple13)] Gary is young.[(triple14 OR ((triple8) -> rule3) OR ((((triple12 triple10) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple3 triple5) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple5 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple8
((triple12 triple10) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
((triple10 triple12) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple12
Gary is white.
("Gary" "is" "white" "+")
triple13
Gary is young.
("Gary" "is" "young" "+")
triple14
((triple8) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple12 triple10) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2