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