Bob is big. If something is kind and red then it is not big. If something is quiet then it is blue. If something is big and not furry then it is blue. If Bob is quiet then Bob is kind. All big things are quiet. If Bob is blue and Bob is not kind then Bob is young.
Bob is big.
("Bob" "is" "big" "+")
If something is kind and red then it is not big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "-"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is big and not furry then it is blue.
((("something" "is" "big" "+") ("something" "is" "furry" "~")) -> ("something" "is" "blue" "+"))
If Bob is quiet then Bob is kind.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "kind" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Bob is blue and Bob is not kind then Bob is young.
((("Bob" "is" "blue" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "young" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is big.[(triple1)] @1: Bob is quiet.[(((triple1) -> rule5))] @2: Bob is blue.[(((((triple1) -> rule5)) -> rule2))] Bob is kind.[(((((triple1) -> rule5)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2