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