Anne is kind. Anne is not rough. Anne is not white. Bob is green. Charlie is blue. Charlie is cold. Charlie is green. Charlie is rough. Charlie is white. Erin is cold. Erin is kind. If something is kind and green then it is white. If something is blue and cold then it is rough. Kind, cold things are blue. Green things are kind. If something is white then it is cold.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is not white.
("Anne" "is" "white" "-")
Bob is green.
("Bob" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
If something is kind and green then it is white.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is blue and cold then it is rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Kind, cold things are blue.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Erin is kind.
True
1
proof
[(triple11)]
("Erin" "is" "kind" "+")
triple11
Charlie is not white.
False
1
inv-proof
[(triple9 OR ((((triple7) -> rule4) triple7) -> rule1))]
("Charlie" "is" "white" "-")
triple9
((((triple7) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is blue.
True
3
proof
[(((triple11 triple10) -> rule3))]
("Erin" "is" "blue" "+")
((triple11 triple10) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple4) -> rule4))]
("Bob" "is" "kind" "-")
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is rough.
True
5
proof
[(((((triple11 triple10) -> rule3) triple10) -> rule2))]
("Erin" "is" "rough" "+")
((((triple11 triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not rough.
False
5
inv-proof
[(((((triple11 triple10) -> rule3) triple10) -> rule2))]
("Erin" "is" "rough" "-")
((((triple11 triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is cold.
True
5
proof
[(((((((triple4) -> rule4) triple4) -> rule1)) -> rule5))]
("Bob" "is" "cold" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not cold.
False
5
inv-proof
[(((((((triple4) -> rule4) triple4) -> rule1)) -> rule5))]
("Bob" "is" "cold" "-")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is blue.
True
8
proof
[(((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "blue" "+")
((((triple4) -> (rule4 % int4)) ((((((triple4) -> (rule4 % int4)) triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not blue.
False
8
inv-proof
[(((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3))]
("Bob" "is" "blue" "-")
((((triple4) -> (rule4 % int4)) ((((((triple4) -> (rule4 % int4)) triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is rough.
True
14
proof
[(((((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule2))]
("Bob" "is" "rough" "+")
((((((triple4) -> (rule4 % int5)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is not rough.
False
14
inv-proof
[(((((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule2))]
("Bob" "is" "rough" "-")
((((((triple4) -> (rule4 % int5)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "white" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is kind.[(triple1)] Anne is not rough.[(triple2)] Anne is not white.[(triple3)] Bob is green.[(triple4)] Charlie is blue.[(triple5 OR ((((triple7) -> rule4) triple6) -> rule3) OR ((((triple7) -> rule4) ((triple9) -> rule5)) -> rule3) OR ((((triple7) -> rule4) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule3))] Charlie is cold.[(triple6 OR ((triple9) -> rule5) OR ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5))] Charlie is green.[(triple7)] Charlie is rough.[(triple8 OR ((triple5 triple6) -> rule2) OR ((triple5 ((triple9) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) triple6) -> rule3) triple6) -> rule2) OR ((((((triple7) -> rule4) triple6) -> rule3) ((triple9) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) ((triple9) -> rule5)) -> rule3) triple6) -> rule2) OR ((((((triple7) -> rule4) ((triple9) -> rule5)) -> rule3) ((triple9) -> rule5)) -> rule2) OR ((triple5 ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) triple6) -> rule3) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) ((triple9) -> rule5)) -> rule3) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule3) triple6) -> rule2) OR ((((((triple7) -> rule4) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule3) ((triple9) -> rule5)) -> rule2) OR ((((((triple7) -> rule4) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule3) ((((((triple7) -> rule4) triple7) -> rule1)) -> rule5)) -> rule2))] Charlie is white.[(triple9 OR ((((triple7) -> rule4) triple7) -> rule1))] Erin is cold.[(triple10)] Erin is kind.[(triple11)] @1: Bob is kind.[(((triple4) -> rule4))] Charlie is kind.[(((triple7) -> rule4))] Erin is blue.[(((triple11 triple10) -> rule3))] @2: Bob is white.[(((((triple4) -> rule4) triple4) -> rule1))] Erin is rough.[(((((triple11 triple10) -> rule3) triple10) -> rule2))] @3: Bob is cold.[(((((((triple4) -> rule4) triple4) -> rule1)) -> rule5))] @4: Bob is blue.[(((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3))] @5: Bob is rough.[(((((((triple4) -> rule4) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule3) ((((((triple4) -> rule4) triple4) -> rule1)) -> rule5)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Anne is not white.
("Anne" "is" "white" "-")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((((triple7) -> (rule4 % int2)) triple6) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule4 % int3)) ((triple9) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple7) -> (rule4 % int4)) ((((((triple7) -> (rule4 % int4)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((triple9) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((((triple7) -> (rule4 % int3)) triple7) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
((triple5 triple6) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5 ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple7) -> (rule4 % int3)) triple6) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple7) -> (rule4 % int4)) triple6) -> (rule3 % int3)) ((triple9) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((triple7) -> (rule4 % int4)) ((triple9) -> (rule5 % int3))) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((triple7) -> (rule4 % int4)) ((triple9) -> (rule5 % int3))) -> (rule3 % int2)) ((triple9) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((triple5 ((((((triple7) -> (rule4 % int4)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((((triple7) -> (rule4 % int5)) triple6) -> (rule3 % int4)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((triple7) -> (rule4 % int5)) ((triple9) -> (rule5 % int4))) -> (rule3 % int3)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int2))) -> (rule5 % int4))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((triple7) -> (rule4 % int5)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((triple7) -> (rule4 % int5)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((triple9) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
((((((triple7) -> (rule4 % int5)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple7) -> (rule4 % int5)) triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
int5
Charlie is white.
("Charlie" "is" "white" "+")
triple9
((((triple7) -> (rule4 % int2)) triple7) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Bob is kind.
("Bob" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple7) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple11 triple10) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple11 triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule1 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
((((triple4) -> (rule4 % int4)) ((((((triple4) -> (rule4 % int4)) triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple4) -> (rule4 % int5)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((((triple4) -> (rule4 % int5)) triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5