Anne is blue. Anne is smart. Charlie is big. Charlie is kind. Charlie is rough. Charlie is not smart. Dave is red. Dave is rough. Dave is smart. Erin is big. Erin is blue. Erin is smart. If Erin is not smart then Erin is rough. If something is blue and smart then it is cold. If something is kind and smart then it is rough. If Erin is rough and Erin is not smart then Erin is not kind. If Erin is cold and Erin is big then Erin is kind. If something is rough and not cold then it is not kind. If something is blue and rough then it is kind. If something is cold and rough then it is big.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is not smart then Erin is rough.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "rough" "+"))
If something is blue and smart then it is cold.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If something is kind and smart then it is rough.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Erin is rough and Erin is not smart then Erin is not kind.
((("Erin" "is" "rough" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "kind" "-"))
If Erin is cold and Erin is big then Erin is kind.
((("Erin" "is" "cold" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "kind" "+"))
If something is rough and not cold then it is not kind.
((("something" "is" "rough" "+") ("something" "is" "cold" "~")) -> ("something" "is" "kind" "-"))
If something is blue and rough then it is kind.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is cold and rough then it is big.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Charlie is not smart.
True
1
proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
Erin is not big.
False
1
inv-proof
[(triple10)]
("Erin" "is" "big" "-")
triple10
Anne is cold.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "cold" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Anne" "is" "cold" "-")
((triple1 triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is kind.
True
5
proof
[(((((triple11 triple12) -> rule2) triple10) -> rule5))]
("Erin" "is" "kind" "+")
((((triple11 triple12) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not kind.
False
5
inv-proof
[(((((triple11 triple12) -> rule2) triple10) -> rule5))]
("Erin" "is" "kind" "-")
((((triple11 triple12) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
True
7
proof
[(((((((triple11 triple12) -> rule2) triple10) -> rule5) triple12) -> rule3))]
("Erin" "is" "rough" "+")
((((((triple11 triple12) -> (rule2 % int3)) triple10) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not rough.
False
7
inv-proof
[(((((((triple11 triple12) -> rule2) triple10) -> rule5) triple12) -> rule3))]
("Erin" "is" "rough" "-")
((((((triple11 triple12) -> (rule2 % int3)) triple10) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is big.
Unknown
rconc
[@3: Anne is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- FAIL)]]
("Anne" "is" "big" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is smart.[(triple2)] Charlie is big.[(triple3)] Charlie is kind.[(triple4)] Charlie is not smart.[(triple6)] Charlie is rough.[(triple5)] Dave is red.[(triple7)] Dave is rough.[(triple8)] Dave is smart.[(triple9)] Erin is big.[(triple10)] Erin is blue.[(triple11)] Erin is smart.[(triple12)] @1: Anne is cold.[(((triple1 triple2) -> rule2))] Erin is cold.[(((triple11 triple12) -> rule2))] @2: Erin is kind.[(((((triple11 triple12) -> rule2) triple10) -> rule5))] @3: Erin is rough.[(((((((triple11 triple12) -> rule2) triple10) -> rule5) triple12) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Erin is big.
("Erin" "is" "big" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple11 triple12) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple11 triple12) -> (rule2 % int2)) triple10) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple11 triple12) -> (rule2 % int3)) triple10) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3