Bob is nice. Dave is white. Erin is red. If Bob is red then Bob is quiet. If something is quiet and not young then it is not white. All white, young things are nice. All red things are not nice. If something is nice then it is quiet. If something is quiet and nice then it is round. If Dave is nice then Dave is not furry. If something is quiet and not nice then it is furry.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
If Bob is red then Bob is quiet.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "quiet" "+"))
If something is quiet and not young then it is not white.
((("something" "is" "quiet" "+") ("something" "is" "young" "~")) -> ("something" "is" "white" "-"))
All white, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All red things are not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and nice then it is round.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Dave is nice then Dave is not furry.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "furry" "-"))
If something is quiet and not nice then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Erin is not nice.
True
2
proof
[(((triple3) -> rule4))]
("Erin" "is" "nice" "-")
((triple3) -> (rule4 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is nice.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Bob is round.
True
4
proof
[(((((triple1) -> rule5) triple1) -> rule6))]
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple1) -> rule5) triple1) -> rule6))]
("Bob" "is" "round" "-")
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is nice.[(triple1)] Dave is white.[(triple2)] Erin is red.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule5))] Erin is not nice.[(((triple3) -> rule4))] @2: Bob is round.[(((((triple1) -> rule5) triple1) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is not nice.
("Erin" "is" "nice" "-")
((triple3) -> (rule4 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2