Anne is quiet. Erin is green. Gary is green. Quiet people are round. Green people are quiet. Young people are not nice. All quiet people are nice. All nice, red people are not blue. If someone is green and not quiet then they are not red. Round, nice people are red. Green people are red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is green.
("Gary" "is" "green" "+")
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Young people are not nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All nice, red people are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "-"))
If someone is green and not quiet then they are not red.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "red" "-"))
Round, nice people are red.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Gary is green.
True
1
proof
[(triple3)]
("Gary" "is" "green" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("Erin" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Erin" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
True
6
proof
[(((((((triple2) -> rule2)) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule1) ((((triple2) -> rule2)) -> rule4)) -> rule7)) -> rule5))]
("Erin" "is" "blue" "-")
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) ((((((triple2) -> (rule2 % int5))) -> (rule1 % int3)) ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Erin is blue.
False
6
inv-proof
[(((((((triple2) -> rule2)) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule1) ((((triple2) -> rule2)) -> rule4)) -> rule7)) -> rule5))]
("Erin" "is" "blue" "+")
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) ((((((triple2) -> (rule2 % int5))) -> (rule1 % int3)) ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is quiet.[(triple1)] Erin is green.[(triple2)] Gary is green.[(triple3)] @1: Anne is nice.[(((triple1) -> rule4))] Anne is round.[(((triple1) -> rule1))] Erin is quiet.[(((triple2) -> rule2))] Erin is red.[(((triple2) -> rule8) OR ((((((triple2) -> rule2)) -> rule1) ((((triple2) -> rule2)) -> rule4)) -> rule7))] Gary is quiet.[(((triple3) -> rule2))] Gary is red.[(((triple3) -> rule8) OR ((((((triple3) -> rule2)) -> rule1) ((((triple3) -> rule2)) -> rule4)) -> rule7))] @2: Anne is red.[(((((triple1) -> rule1) ((triple1) -> rule4)) -> rule7))] Erin is nice.[(((((triple2) -> rule2)) -> rule4))] Erin is round.[(((((triple2) -> rule2)) -> rule1))] Gary is nice.[(((((triple3) -> rule2)) -> rule4))] Gary is round.[(((((triple3) -> rule2)) -> rule1))] @3: Anne is not blue.[(((((triple1) -> rule4) ((((triple1) -> rule1) ((triple1) -> rule4)) -> rule7)) -> rule5))] Erin is not blue.[(((((((triple2) -> rule2)) -> rule4) ((triple2) -> rule8)) -> rule5) OR ((((((triple2) -> rule2)) -> rule4) ((((((triple2) -> rule2)) -> rule1) ((((triple2) -> rule2)) -> rule4)) -> rule7)) -> rule5))] Gary is not blue.[(((((((triple3) -> rule2)) -> rule4) ((triple3) -> rule8)) -> rule5) OR ((((((triple3) -> rule2)) -> rule4) ((((((triple3) -> rule2)) -> rule1) ((((triple3) -> rule2)) -> rule4)) -> rule7)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((((triple2) -> (rule2 % int4))) -> (rule1 % int3)) ((((triple2) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((((triple3) -> (rule2 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int3)) ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Anne is not blue.
("Anne" "is" "blue" "-")
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule1 % int3)) ((triple1) -> (rule4 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple2) -> (rule2 % int4))) -> (rule4 % int3)) ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
((((((triple2) -> (rule2 % int5))) -> (rule4 % int4)) ((((((triple2) -> (rule2 % int5))) -> (rule1 % int3)) ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is quiet.
("Erin" "is" "quiet" "+")
int5
Gary is not blue.
("Gary" "is" "blue" "-")
((((((triple3) -> (rule2 % int4))) -> (rule4 % int3)) ((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((triple3) -> (rule2 % int5))) -> (rule4 % int4)) ((((((triple3) -> (rule2 % int5))) -> (rule1 % int3)) ((((triple3) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5