Bob is big. Bob is round. Dave is smart. Dave is young. Gary is rough. Gary is round. Gary is young. All big people are rough. If someone is big then they are round. Big, rough people are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Big, rough people are furry.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Gary is young.
True
1
proof
[(triple7)]
("Gary" "is" "young" "+")
triple7
Bob is not round.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule2))]
("Bob" "is" "round" "-")
triple2
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is big.[(triple1)] Bob is round.[(triple2 OR ((triple1) -> rule2))] Dave is smart.[(triple3)] Dave is young.[(triple4)] Gary is rough.[(triple5)] Gary is round.[(triple6)] Gary is young.[(triple7)] @1: Bob is rough.[(((triple1) -> rule1))] @2: Bob is furry.[(((triple1 ((triple1) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2