Anne is not quiet. Anne is white. Erin is round. Gary is blue. Gary is quiet. Gary is red. Gary is rough. Gary is round. Gary is young. Harry is not young. All blue, young people are red. All white, rough people are red. If someone is young and red then they are blue. If someone is white and round then they are rough. White people are round. All red people are round. If Gary is white and Gary is blue then Gary is not rough. If someone is red and round then they are young. If someone is round and not white then they are quiet.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is white.
("Anne" "is" "white" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not young.
("Harry" "is" "young" "-")
All blue, young people are red.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All white, rough people are red.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is young and red then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is white and round then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Gary is white and Gary is blue then Gary is not rough.
((("Gary" "is" "white" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "rough" "-"))
If someone is red and round then they are young.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is round and not white then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Erin is round.
True
1
proof
[(triple3)]
("Erin" "is" "round" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple9 OR ((triple6 triple8) -> rule8) OR ((triple6 ((triple6) -> rule6)) -> rule8))]
("Gary" "is" "young" "-")
triple9
((triple6 triple8) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Anne is round.
True
2
proof
[(((triple2) -> rule5))]
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple2) -> rule5))]
("Anne" "is" "round" "-")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule4))]
("Anne" "is" "rough" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule4))]
("Anne" "is" "rough" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
True
6
proof
[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "red" "+")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not red.
False
6
inv-proof
[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))]
("Anne" "is" "red" "-")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
True
9
proof
[(((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8))]
("Anne" "is" "young" "+")
((((triple2 ((triple2 ((triple2) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule5 % int4))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not young.
False
9
inv-proof
[(((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8))]
("Anne" "is" "young" "-")
((((triple2 ((triple2 ((triple2) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule5 % int4))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is blue.
True
16
proof
[(((((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8) ((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2)) -> rule3))]
("Anne" "is" "blue" "+")
((((((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple2) -> (rule5 % int5))) -> (rule8 % int2)) ((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Anne is not blue.
False
16
inv-proof
[(((((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8) ((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2)) -> rule3))]
("Anne" "is" "blue" "-")
((((((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple2) -> (rule5 % int5))) -> (rule8 % int2)) ((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "rough" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Erin is red.
Unknown
rconc
[@3: Erin is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Erin" "is" "red" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is not quiet.[(triple1)] Anne is white.[(triple2)] Erin is round.[(triple3)] Gary is blue.[(triple4 OR ((triple9 triple6) -> rule3) OR ((((triple6 triple8) -> rule8) triple6) -> rule3) OR ((((triple6 ((triple6) -> rule6)) -> rule8) triple6) -> rule3))] Gary is quiet.[(triple5)] Gary is red.[(triple6 OR ((triple4 triple9) -> rule1))] Gary is rough.[(triple7)] Gary is round.[(triple8 OR ((triple6) -> rule6) OR ((((triple4 triple9) -> rule1)) -> rule6))] Gary is young.[(triple9 OR ((triple6 triple8) -> rule8) OR ((triple6 ((triple6) -> rule6)) -> rule8))] Harry is not young.[(triple10)] @1: Anne is round.[(((triple2) -> rule5))] @2: Anne is rough.[(((triple2 ((triple2) -> rule5)) -> rule4))] @3: Anne is red.[(((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2))] @4: Anne is young.[(((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8))] @5: Anne is blue.[(((((((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2) ((triple2) -> rule5)) -> rule8) ((triple2 ((triple2 ((triple2) -> rule5)) -> rule4)) -> rule2)) -> rule3))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Erin is round.
("Erin" "is" "round" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
((triple9 triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple6 triple8) -> (rule8 % int2)) triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((triple6 ((triple6) -> (rule6 % int3))) -> (rule8 % int2)) triple6) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple4 triple9) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
((triple6) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple4 triple9) -> (rule1 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple9
((triple6 triple8) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule6 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple2 ((triple2 ((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((triple2 ((triple2) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2) -> (rule5 % int4))) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3)) ((triple2) -> (rule5 % int5))) -> (rule8 % int2)) ((triple2 ((triple2 ((triple2) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
int4
Anne is round.
("Anne" "is" "round" "+")
int5