Charlie is quiet. Charlie is round. Dave is green. Dave is kind. Erin is not furry. Erin is green. Erin is kind. Erin is nice. Erin is round. Fiona is furry. Fiona is not green. Fiona is not kind. Fiona is nice. Fiona is quiet. Fiona is round. Fiona is not white. If Erin is green then Erin is white. White people are nice. Nice, kind people are quiet. If Charlie is round then Charlie is quiet. If Dave is white then Dave is nice. Kind people are white.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
If Erin is green then Erin is white.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "white" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Nice, kind people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is round then Charlie is quiet.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "quiet" "+"))
If Dave is white then Dave is nice.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Fiona is furry.
True
1
proof
[(triple10)]
("Fiona" "is" "furry" "+")
triple10
Erin is not green.
False
1
inv-proof
[(triple6)]
("Erin" "is" "green" "-")
triple6
Dave is white.
True
2
proof
[(((triple4) -> rule6))]
("Dave" "is" "white" "+")
((triple4) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is not quiet.
False
3
inv-proof
[(((triple8 triple7) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple7) -> rule3) OR ((((((triple7) -> rule6)) -> rule2) triple7) -> rule3))]
("Erin" "is" "quiet" "-")
((triple8 triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Dave is nice.
True
3
proof
[(((((triple4) -> rule6)) -> rule2) OR ((((triple4) -> rule6)) -> rule5))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule2) OR ((((triple4) -> rule6)) -> rule5))]
("Dave" "is" "nice" "-")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
True
5
proof
[(((((((triple4) -> rule6)) -> rule2) triple4) -> rule3) OR ((((((triple4) -> rule6)) -> rule5) triple4) -> rule3))]
("Dave" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not quiet.
False
5
inv-proof
[(((((((triple4) -> rule6)) -> rule2) triple4) -> rule3) OR ((((((triple4) -> rule6)) -> rule5) triple4) -> rule3))]
("Dave" "is" "quiet" "-")
((((((triple4) -> (rule6 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is nice.
Unknown
rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is quiet.[(triple1 OR ((triple2) -> rule4))] Charlie is round.[(triple2)] Dave is green.[(triple3)] Dave is kind.[(triple4)] Erin is green.[(triple6)] Erin is kind.[(triple7)] Erin is nice.[(triple8 OR ((((triple6) -> rule1)) -> rule2) OR ((((triple7) -> rule6)) -> rule2))] Erin is not furry.[(triple5)] Erin is round.[(triple9)] Fiona is furry.[(triple10)] Fiona is nice.[(triple13)] Fiona is not green.[(triple11)] Fiona is not kind.[(triple12)] Fiona is not white.[(triple16)] Fiona is quiet.[(triple14)] Fiona is round.[(triple15)] @1: Dave is white.[(((triple4) -> rule6))] Erin is quiet.[(((triple8 triple7) -> rule3) OR ((((((triple6) -> rule1)) -> rule2) triple7) -> rule3) OR ((((((triple7) -> rule6)) -> rule2) triple7) -> rule3))] Erin is white.[(((triple6) -> rule1) OR ((triple7) -> rule6))] @2: Dave is nice.[(((((triple4) -> rule6)) -> rule2) OR ((((triple4) -> rule6)) -> rule5))] @3: Dave is quiet.[(((((((triple4) -> rule6)) -> rule2) triple4) -> rule3) OR ((((((triple4) -> rule6)) -> rule5) triple4) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not furry.
("Erin" "is" "furry" "-")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Fiona is not green.
("Fiona" "is" "green" "-")
triple11
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple12
Fiona is not white.
("Fiona" "is" "white" "-")
triple16
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
Fiona is round.
("Fiona" "is" "round" "+")
triple15
Dave is white.
("Dave" "is" "white" "+")
((triple4) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple8 triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((((triple6) -> (rule1 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple7) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple4) -> (rule6 % int3))) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((triple4) -> (rule6 % int3))) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3