Anne is blue. Erin is kind. Harry is cold. Kind things are quiet. If Anne is big then Anne is nice. All big things are nice. If Erin is quiet and Erin is nice then Erin is furry. If Anne is big and Anne is blue then Anne is nice. If Anne is kind and Anne is blue then Anne is cold. If Harry is blue and Harry is cold then Harry is nice. Blue things are big.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Anne is big then Anne is nice.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "nice" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Erin is quiet and Erin is nice then Erin is furry.
((("Erin" "is" "quiet" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "furry" "+"))
If Anne is big and Anne is blue then Anne is nice.
((("Anne" "is" "big" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "nice" "+"))
If Anne is kind and Anne is blue then Anne is cold.
((("Anne" "is" "kind" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
If Harry is blue and Harry is cold then Harry is nice.
((("Harry" "is" "blue" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "nice" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "big" "+")
((triple1) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "big" "-")
((triple1) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule8)) -> rule2) OR ((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8) triple1) -> rule5))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule2) OR ((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8) triple1) -> rule5))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "big" "+")
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Harry" "is" "nice" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Erin is kind.[(triple2)] Harry is cold.[(triple3)] @1: Anne is big.[(((triple1) -> rule8))] Erin is quiet.[(((triple2) -> rule1))] @2: Anne is nice.[(((((triple1) -> rule8)) -> rule2) OR ((((triple1) -> rule8)) -> rule3) OR ((((triple1) -> rule8) triple1) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple1) -> (rule8 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2