Dave is not green. Dave is round. Dave is white. Fiona is furry. Fiona is red. Fiona is round. Fiona is white. Gary is not green. Gary is round. Gary is white. If something is nice then it is quiet. If something is furry and white then it is quiet. If something is quiet then it is red. All red, green things are round. If Dave is white then Dave is red. All round things are white. If Fiona is furry then Fiona is red. If something is red then it is nice.
Dave is not green.
("Dave" "is" "green" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and white then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
All red, green things are round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Dave is white then Dave is red.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "red" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
If Fiona is furry then Fiona is red.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "red" "+"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Fiona is furry.
True
1
proof
[(triple4)]
("Fiona" "is" "furry" "+")
triple4
Gary is not round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "-")
triple9
Fiona is nice.
True
2
proof
[(((triple5) -> rule8) OR ((((triple4) -> rule7)) -> rule8) OR ((((((triple4 triple7) -> rule2)) -> rule3)) -> rule8) OR ((((((triple4 ((triple6) -> rule6)) -> rule2)) -> rule3)) -> rule8))]
("Fiona" "is" "nice" "+")
((triple5) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple4 triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((((triple4 ((triple6) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is not quiet.
False
3
inv-proof
[(((triple4 triple7) -> rule2) OR ((((triple5) -> rule8)) -> rule1) OR ((triple4 ((triple6) -> rule6)) -> rule2) OR ((((((triple4) -> rule7)) -> rule8)) -> rule1))]
("Fiona" "is" "quiet" "-")
((triple4 triple7) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple4 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Dave is nice.
True
3
proof
[(((((triple3) -> rule5)) -> rule8) OR ((((((triple2) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not nice.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule8) OR ((((((triple2) -> rule6)) -> rule5)) -> rule8))]
("Dave" "is" "nice" "-")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
True
4
proof
[(((((((triple3) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule5)) -> rule8)) -> rule1))]
("Dave" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule5)) -> rule8)) -> rule1))]
("Dave" "is" "quiet" "-")
((((((triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule8 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not quiet.
Unknown
inv-rconc
[@4: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule3 <- rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Dave is not green.[(triple1)] Dave is round.[(triple2)] Dave is white.[(triple3 OR ((triple2) -> rule6))] Fiona is furry.[(triple4)] Fiona is red.[(triple5 OR ((triple4) -> rule7) OR ((((triple4 triple7) -> rule2)) -> rule3) OR ((((triple4 ((triple6) -> rule6)) -> rule2)) -> rule3))] Fiona is round.[(triple6)] Fiona is white.[(triple7 OR ((triple6) -> rule6))] Gary is not green.[(triple8)] Gary is round.[(triple9)] Gary is white.[(triple10 OR ((triple9) -> rule6))] @1: Dave is red.[(((triple3) -> rule5) OR ((((triple2) -> rule6)) -> rule5))] Fiona is nice.[(((triple5) -> rule8) OR ((((triple4) -> rule7)) -> rule8) OR ((((((triple4 triple7) -> rule2)) -> rule3)) -> rule8) OR ((((((triple4 ((triple6) -> rule6)) -> rule2)) -> rule3)) -> rule8))] Fiona is quiet.[(((triple4 triple7) -> rule2) OR ((((triple5) -> rule8)) -> rule1) OR ((triple4 ((triple6) -> rule6)) -> rule2) OR ((((((triple4) -> rule7)) -> rule8)) -> rule1))] @2: Dave is nice.[(((((triple3) -> rule5)) -> rule8) OR ((((((triple2) -> rule6)) -> rule5)) -> rule8))] @3: Dave is quiet.[(((((((triple3) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple2) -> rule6)) -> rule5)) -> rule8)) -> rule1))]
Dave is not green.
("Dave" "is" "green" "-")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
((triple2) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
((triple4) -> (rule7 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple4 triple7) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple4 ((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
((triple9) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple5) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple4 triple7) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((((triple4 ((triple6) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
int4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple4 triple7) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple4 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4