Bob is big. Bob is green. Bob is rough. Gary is big. Gary is green. Gary is quiet. Gary is smart. Smart things are blue. All rough, big things are not young.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
All rough, big things are not young.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
Gary is smart.
True
1
proof
[(triple7)]
("Gary" "is" "smart" "+")
triple7
Gary is not green.
False
1
inv-proof
[(triple5)]
("Gary" "is" "green" "-")
triple5
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is rough.[(triple3)] Gary is big.[(triple4)] Gary is green.[(triple5)] Gary is quiet.[(triple6)] Gary is smart.[(triple7)] @1: Bob is not young.[(((triple3 triple1) -> rule2))] Gary is blue.[(((triple7) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Bob is not young.
("Bob" "is" "young" "-")
((triple3 triple1) -> (rule2 % int1))
Bob is not young.
("Bob" "is" "young" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1