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