Bob is blue. Bob is quiet. Bob is red. Bob is round. Bob is young. Charlie is blue. Charlie is quiet. All round people are young. All red people are furry. Rough people are round. Round, quiet people are furry. If someone is furry and blue then they are young. All young, furry people are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Round, quiet people are furry.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and blue then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All young, furry people are round.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Bob is young.
True
1
proof
[(triple5 OR ((triple4) -> rule1) OR ((((triple3) -> rule2) triple1) -> rule5) OR ((((triple4 triple2) -> rule4) triple1) -> rule5))]
("Bob" "is" "young" "+")
triple5
((triple4) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple4 triple2) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is furry.
True
2
proof
[(((triple3) -> rule2) OR ((triple4 triple2) -> rule4))]
("Bob" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple4 triple2) -> rule4))]
("Bob" "is" "furry" "-")
((triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@3: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is round.
Unknown
rconc
[@3: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule3 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Bob is round.[(triple4 OR ((triple5 ((triple3) -> rule2)) -> rule6) OR ((((((triple3) -> rule2) triple1) -> rule5) ((triple3) -> rule2)) -> rule6))] Bob is young.[(triple5 OR ((triple4) -> rule1) OR ((((triple3) -> rule2) triple1) -> rule5) OR ((((triple4 triple2) -> rule4) triple1) -> rule5))] Charlie is blue.[(triple6)] Charlie is quiet.[(triple7)] @1: Bob is furry.[(((triple3) -> rule2) OR ((triple4 triple2) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple5 ((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple3) -> (rule2 % int3)) triple1) -> (rule5 % int2)) ((triple3) -> (rule2 % int3))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple5
((triple4) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple3) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple4 triple2) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1