Bob is big. Bob is blue. Charlie is green. Charlie is round. Gary is big. Gary is furry. Gary is smart. If Bob is blue and Bob is white then Bob is green. If something is big and smart then it is blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Bob is blue and Bob is white then Bob is green.
((("Bob" "is" "blue" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "green" "+"))
If something is big and smart then it is blue.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Charlie is round.
True
1
proof
[(triple4)]
("Charlie" "is" "round" "+")
triple4
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Gary is blue.
True
3
proof
[(((triple5 triple7) -> rule2))]
("Gary" "is" "blue" "+")
((triple5 triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("Gary" "is" "blue" "-")
((triple5 triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Charlie is green.[(triple3)] Charlie is round.[(triple4)] Gary is big.[(triple5)] Gary is furry.[(triple6)] Gary is smart.[(triple7)] @1: Gary is blue.[(((triple5 triple7) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
((triple5 triple7) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1