Anne is furry. Charlie is red. Erin is big. All nice, blue things are big. If something is cold and furry then it is kind. Nice things are kind. If Anne is nice and Anne is not furry then Anne is blue. All kind things are cold. All red things are nice. If Anne is kind and Anne is nice then Anne is big. If Anne is big and Anne is nice then Anne is red.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
All nice, blue things are big.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is cold and furry then it is kind.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Anne is nice and Anne is not furry then Anne is blue.
((("Anne" "is" "nice" "+") ("Anne" "is" "furry" "~")) -> ("Anne" "is" "blue" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Anne is kind and Anne is nice then Anne is big.
((("Anne" "is" "kind" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "big" "+"))
If Anne is big and Anne is nice then Anne is red.
((("Anne" "is" "big" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "red" "+"))
Erin is big.
True
1
proof
[(triple3)]
("Erin" "is" "big" "+")
triple3
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Charlie is nice.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
True
4
proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not cold.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
("Charlie" "is" "cold" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is not red.
Unknown
inv-rconc
[@2: Anne is red.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Anne" "is" "red" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "nice" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Charlie is red.[(triple2)] Erin is big.[(triple3)] @1: Charlie is nice.[(((triple2) -> rule6))] @2: Charlie is kind.[(((((triple2) -> rule6)) -> rule3))] @3: Charlie is cold.[(((((((triple2) -> rule6)) -> rule3)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3