Anne is cold. Anne is rough. Charlie is quiet. Charlie is not rough. Charlie is young. Fiona is cold. Fiona is quiet. Gary is rough. Gary is white. Gary is young. If someone is young and not kind then they are not white. All quiet, green people are white. If someone is cold then they are green. If someone is kind then they are not green. All quiet people are green. All cold people are quiet. All white people are cold. If someone is quiet and kind then they are cold.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is young and not kind then they are not white.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "white" "-"))
All quiet, green people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is kind then they are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
All cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and kind then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Charlie is young.
True
1
proof
[(triple5)]
("Charlie" "is" "young" "+")
triple5
Anne is not rough.
False
1
inv-proof
[(triple2)]
("Anne" "is" "rough" "-")
triple2
Gary is cold.
True
2
proof
[(((triple9) -> rule7))]
("Gary" "is" "cold" "+")
((triple9) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
True
5
proof
[(((((triple1) -> rule6) ((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule5)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is not white.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule2))]
("Charlie" "is" "white" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is cold.
True
5
proof
[(((((triple3 ((triple3) -> rule5)) -> rule2)) -> rule7))]
("Charlie" "is" "cold" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule5)) -> rule2)) -> rule7))]
("Charlie" "is" "cold" "-")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is cold.[(triple1)] Anne is rough.[(triple2)] Charlie is not rough.[(triple4)] Charlie is quiet.[(triple3)] Charlie is young.[(triple5)] Fiona is cold.[(triple6 OR ((((triple7 ((triple7) -> rule5)) -> rule2)) -> rule7))] Fiona is quiet.[(triple7 OR ((triple6) -> rule6))] Gary is rough.[(triple8)] Gary is white.[(triple9)] Gary is young.[(triple10)] @1: Anne is green.[(((triple1) -> rule3) OR ((((triple1) -> rule6)) -> rule5))] Anne is quiet.[(((triple1) -> rule6))] Charlie is green.[(((triple3) -> rule5))] Fiona is green.[(((triple6) -> rule3) OR ((triple7) -> rule5) OR ((((triple6) -> rule6)) -> rule5))] Gary is cold.[(((triple9) -> rule7))] @2: Anne is white.[(((((triple1) -> rule6) ((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule5)) -> rule2))] Charlie is white.[(((triple3 ((triple3) -> rule5)) -> rule2))] Fiona is white.[(((triple7 ((triple6) -> rule3)) -> rule2) OR ((triple7 ((triple7) -> rule5)) -> rule2) OR ((((triple6) -> rule6) ((triple6) -> rule3)) -> rule2) OR ((((triple6) -> rule6) ((triple7) -> rule5)) -> rule2) OR ((triple7 ((((triple6) -> rule6)) -> rule5)) -> rule2) OR ((((triple6) -> rule6) ((((triple6) -> rule6)) -> rule5)) -> rule2))] Gary is green.[(((((triple9) -> rule7)) -> rule3) OR ((((((triple9) -> rule7)) -> rule6)) -> rule5))] Gary is quiet.[(((((triple9) -> rule7)) -> rule6))] @3: Charlie is cold.[(((((triple3 ((triple3) -> rule5)) -> rule2)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((((triple7 ((triple7) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((triple6) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is white.
("Gary" "is" "white" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple3) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple6) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple7) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((triple9) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((triple7 ((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple6) -> (rule6 % int3)) ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((triple6) -> (rule6 % int3)) ((triple7) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((triple7 ((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((triple6) -> (rule6 % int3)) ((((triple6) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((((((triple9) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3