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