Bob is not green. Bob is quiet. Bob is red. Bob is round. Dave is blue. Dave is furry. Dave is not green. Dave is quiet. Dave is round. Dave is young. If Dave is quiet and Dave is red then Dave is round. All green, quiet people are young. If someone is green then they are round. If someone is red and furry then they are round. Red people are furry. Blue, red people are furry. If Bob is green and Bob is blue then Bob is red. All young, green people are red.
Bob is not green.
("Bob" "is" "green" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
If Dave is quiet and Dave is red then Dave is round.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "round" "+"))
All green, quiet people are young.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is red and furry then they are round.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Blue, red people are furry.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Bob is green and Bob is blue then Bob is red.
((("Bob" "is" "green" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
All young, green people are red.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Dave is young.
True
1
proof
[(triple10)]
("Dave" "is" "young" "+")
triple10
Bob is not round.
False
1
inv-proof
[(triple4 OR ((triple3 ((triple3) -> rule5)) -> rule4))]
("Bob" "is" "round" "-")
triple4
((triple3 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is furry.
True
2
proof
[(((triple3) -> rule5))]
("Bob" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "furry" "-")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "red" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is not green.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4 OR ((triple3 ((triple3) -> rule5)) -> rule4))] Dave is blue.[(triple5)] Dave is furry.[(triple6)] Dave is not green.[(triple7)] Dave is quiet.[(triple8)] Dave is round.[(triple9)] Dave is young.[(triple10)] @1: Bob is furry.[(((triple3) -> rule5))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple3 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is not green.
("Dave" "is" "green" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1