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