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