Anne is cold. Anne is nice. Anne is not rough. Anne is smart. Erin is big. Erin is blue. Erin is kind. Erin is nice. Erin is not smart. Harry is nice. If Erin is smart and Erin is nice then Erin is cold. If something is nice then it is blue. If something is cold and blue then it is not big. Cold things are nice. If something is blue and not nice then it is not rough. If something is blue and not rough then it is kind.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Harry is nice.
("Harry" "is" "nice" "+")
If Erin is smart and Erin is nice then Erin is cold.
((("Erin" "is" "smart" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "cold" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is cold and blue then it is not big.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "-"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is blue and not nice then it is not rough.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "rough" "-"))
If something is blue and not rough then it is kind.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple7)]
("Erin" "is" "kind" "+")
triple7
Erin is not blue.
False
1
inv-proof
[(triple6 OR ((triple8) -> rule2))]
("Erin" "is" "blue" "-")
triple6
((triple8) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is blue.
True
2
proof
[(((triple10) -> rule2))]
("Harry" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple1) -> rule4)) -> rule2))]
("Anne" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is kind.
True
4
proof
[(((((triple2) -> rule2) triple3) -> rule6) OR ((((((triple1) -> rule4)) -> rule2) triple3) -> rule6))]
("Anne" "is" "kind" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((triple2) -> rule2) triple3) -> rule6) OR ((((((triple1) -> rule4)) -> rule2) triple3) -> rule6))]
("Anne" "is" "kind" "-")
((((triple2) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2 OR ((triple1) -> rule4))] Anne is not rough.[(triple3)] Anne is smart.[(triple4)] Erin is big.[(triple5)] Erin is blue.[(triple6 OR ((triple8) -> rule2))] Erin is kind.[(triple7)] Erin is nice.[(triple8)] Erin is not smart.[(triple9)] Harry is nice.[(triple10)] @1: Anne is blue.[(((triple2) -> rule2) OR ((((triple1) -> rule4)) -> rule2))] Harry is blue.[(((triple10) -> rule2))] @2: Anne is kind.[(((((triple2) -> rule2) triple3) -> rule6) OR ((((((triple1) -> rule4)) -> rule2) triple3) -> rule6))] Anne is not big.[(((triple1 ((triple2) -> rule2)) -> rule3) OR ((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
((triple8) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is not smart.
("Erin" "is" "smart" "-")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not big.
("Anne" "is" "big" "-")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3