Bob is not big. Bob is red. Bob is rough. Bob is round. Dave is cold. Dave is not furry. Dave is red. Dave is rough. Dave is round. Dave is young. If Bob is rough then Bob is young. If Bob is round and Bob is rough then Bob is young. If Dave is red and Dave is furry then Dave is rough. If Dave is furry then Dave is young. Young people are red. Furry people are big.
Bob is not big.
("Bob" "is" "big" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Bob is rough then Bob is young.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "young" "+"))
If Bob is round and Bob is rough then Bob is young.
((("Bob" "is" "round" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "young" "+"))
If Dave is red and Dave is furry then Dave is rough.
((("Dave" "is" "red" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "rough" "+"))
If Dave is furry then Dave is young.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "+"))
Young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Dave is young.
True
1
proof
[(triple10)]
("Dave" "is" "young" "+")
triple10
Dave is not round.
False
1
inv-proof
[(triple9)]
("Dave" "is" "round" "-")
triple9
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is not big.[(triple1)] Bob is red.[(triple2 OR ((((triple3) -> rule1)) -> rule5) OR ((((triple4 triple3) -> rule2)) -> rule5))] Bob is rough.[(triple3)] Bob is round.[(triple4)] Dave is cold.[(triple5)] Dave is not furry.[(triple6)] Dave is red.[(triple7 OR ((triple10) -> rule5))] Dave is rough.[(triple8)] Dave is round.[(triple9)] Dave is young.[(triple10)] @1: Bob is young.[(((triple3) -> rule1) OR ((triple4 triple3) -> rule2))]
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple10) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Bob is young.
("Bob" "is" "young" "+")
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1