Bob is white. Dave is white. If Bob is nice and Bob is not white then Bob is furry. All white things are furry. Furry things are quiet. Smart, white things are not kind. If something is quiet and not furry then it is smart. If something is smart and kind then it is red. Furry things are red. If something is furry and not white then it is red.
Bob is white.
("Bob" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
If Bob is nice and Bob is not white then Bob is furry.
((("Bob" "is" "nice" "+") ("Bob" "is" "white" "~")) -> ("Bob" "is" "furry" "+"))
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Smart, white things are not kind.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If something is quiet and not furry then it is smart.
((("something" "is" "quiet" "+") ("something" "is" "furry" "~")) -> ("something" "is" "smart" "+"))
If something is smart and kind then it is red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is furry and not white then it is red.
((("something" "is" "furry" "+") ("something" "is" "white" "~")) -> ("something" "is" "red" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Dave is furry.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule7))]
("Dave" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "smart" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is white.[(triple1)] Dave is white.[(triple2)] @1: Bob is furry.[(((triple1) -> rule2))] Dave is furry.[(((triple2) -> rule2))] @2: Bob is quiet.[(((((triple1) -> rule2)) -> rule3))] Bob is red.[(((((triple1) -> rule2)) -> rule7))] Dave is quiet.[(((((triple2) -> rule2)) -> rule3))] Dave is red.[(((((triple2) -> rule2)) -> rule7))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2