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