Bob is round. Bob is young. Gary is round. All round things are white. If Gary is white and Gary is big then Gary is nice.
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Gary is white and Gary is big then Gary is nice.
((("Gary" "is" "white" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "nice" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Gary is white.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "white" "+")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "white" "-")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is round.[(triple1)] Bob is young.[(triple2)] Gary is round.[(triple3)] @1: Bob is white.[(((triple1) -> rule1))] Gary is white.[(((triple3) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1