Anne is cold. Bob is cold. Bob is kind. Bob is red. Erin is not quiet. Erin is red. Fiona is not cold. Red things are green. Young things are green. If something is cold then it is young. If something is green and kind then it is not blue. If something is blue and not young then it is kind. If something is young then it is kind.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is green and kind then it is not blue.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "-"))
If something is blue and not young then it is kind.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
If something is young then it is kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Bob is red.
True
1
proof
[(triple4)]
("Bob" "is" "red" "+")
triple4
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Erin is green.
True
2
proof
[(((triple6) -> rule1))]
("Erin" "is" "green" "+")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple6) -> rule1))]
("Erin" "is" "green" "-")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is blue.
False
4
inv-proof
[(((((triple4) -> rule1) triple3) -> rule4) OR ((((((triple2) -> rule3)) -> rule2) triple3) -> rule4) OR ((((triple4) -> rule1) ((((triple2) -> rule3)) -> rule6)) -> rule4) OR ((((((triple2) -> rule3)) -> rule2) ((((triple2) -> rule3)) -> rule6)) -> rule4))]
("Bob" "is" "blue" "+")
((((triple4) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple2) -> (rule3 % int4))) -> (rule2 % int3)) ((((triple2) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Anne is not blue.
True
7
proof
[(((((((triple1) -> rule3)) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is blue.
False
7
inv-proof
[(((((((triple1) -> rule3)) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "young" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3 OR ((((triple2) -> rule3)) -> rule6))] Bob is red.[(triple4)] Erin is not quiet.[(triple5)] Erin is red.[(triple6)] Fiona is not cold.[(triple7)] @1: Anne is young.[(((triple1) -> rule3))] Bob is green.[(((triple4) -> rule1) OR ((((triple2) -> rule3)) -> rule2))] Bob is young.[(((triple2) -> rule3))] Erin is green.[(((triple6) -> rule1))] @2: Anne is green.[(((((triple1) -> rule3)) -> rule2))] Anne is kind.[(((((triple1) -> rule3)) -> rule6))] Bob is not blue.[(((((triple4) -> rule1) triple3) -> rule4) OR ((((((triple2) -> rule3)) -> rule2) triple3) -> rule4) OR ((((triple4) -> rule1) ((((triple2) -> rule3)) -> rule6)) -> rule4) OR ((((((triple2) -> rule3)) -> rule2) ((((triple2) -> rule3)) -> rule6)) -> rule4))] @3: Anne is not blue.[(((((((triple1) -> rule3)) -> rule2) ((((triple1) -> rule3)) -> rule6)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
triple4
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple2) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple6) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple4) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple2) -> (rule3 % int4))) -> (rule2 % int3)) ((((triple2) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Anne is not blue.
("Anne" "is" "blue" "-")
((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) ((((triple1) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4