Anne is blue. Anne is cold. Charlie is not blue. Fiona is cold. Gary is not cold. Gary is nice. Gary is red. If something is cold and young then it is red. If something is young and nice then it is red. If Anne is young and Anne is nice then Anne is quiet. All red, cold things are nice. If Gary is blue then Gary is nice. If something is cold then it is young. All quiet, blue things are kind. If something is quiet and young then it is kind. If something is red and not quiet then it is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
If something is cold and young then it is red.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young and nice then it is red.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Anne is young and Anne is nice then Anne is quiet.
((("Anne" "is" "young" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "quiet" "+"))
All red, cold things are nice.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Gary is blue then Gary is nice.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "nice" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All quiet, blue things are kind.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and young then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is red and not quiet then it is kind.
((("something" "is" "red" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "+"))
Fiona is cold.
True
1
proof
[(triple4)]
("Fiona" "is" "cold" "+")
triple4
Charlie is blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "+")
triple3
Fiona is young.
True
2
proof
[(((triple4) -> rule6))]
("Fiona" "is" "young" "+")
((triple4) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "young" "-")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is red.
True
4
proof
[(((triple4 ((triple4) -> rule6)) -> rule1))]
("Fiona" "is" "red" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is not red.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule1))]
("Anne" "is" "red" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is nice.
True
6
proof
[(((((triple4 ((triple4) -> rule6)) -> rule1) triple4) -> rule4))]
("Fiona" "is" "nice" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is not nice.
False
6
inv-proof
[(((((triple4 ((triple4) -> rule6)) -> rule1) triple4) -> rule4))]
("Fiona" "is" "nice" "-")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Anne is quiet.
True
9
proof
[(((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3))]
("Anne" "is" "quiet" "+")
((((triple2) -> (rule6 % int4)) ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is not quiet.
False
9
inv-proof
[(((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3))]
("Anne" "is" "quiet" "-")
((((triple2) -> (rule6 % int4)) ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is kind.
True
11
proof
[(((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) triple1) -> rule7) OR ((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) ((triple2) -> rule6)) -> rule8))]
("Anne" "is" "kind" "+")
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int5))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is not kind.
False
11
inv-proof
[(((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) triple1) -> rule7) OR ((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) ((triple2) -> rule6)) -> rule8))]
("Anne" "is" "kind" "-")
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int5))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "kind" "+")
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Charlie is not blue.[(triple3)] Fiona is cold.[(triple4)] Gary is nice.[(triple6)] Gary is not cold.[(triple5)] Gary is red.[(triple7)] @1: Anne is young.[(((triple2) -> rule6))] Fiona is young.[(((triple4) -> rule6))] @2: Anne is red.[(((triple2 ((triple2) -> rule6)) -> rule1))] Fiona is red.[(((triple4 ((triple4) -> rule6)) -> rule1))] @3: Anne is nice.[(((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4))] Fiona is nice.[(((((triple4 ((triple4) -> rule6)) -> rule1) triple4) -> rule4))] @4: Anne is quiet.[(((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3))] @5: Anne is kind.[(((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) triple1) -> rule7) OR ((((((triple2) -> rule6) ((((triple2 ((triple2) -> rule6)) -> rule1) triple2) -> rule4)) -> rule3) ((triple2) -> rule6)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not cold.
("Gary" "is" "cold" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple4) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple2) -> (rule6 % int4)) ((((triple2 ((triple2) -> (rule6 % int4))) -> (rule1 % int3)) triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
((((((triple2) -> (rule6 % int5)) ((((triple2 ((triple2) -> (rule6 % int5))) -> (rule1 % int4)) triple2) -> (rule4 % int3))) -> (rule3 % int2)) ((triple2) -> (rule6 % int5))) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5