Anne is blue. Anne is cold. Dave is red. Dave is white. Erin is cold. Erin is nice. Erin is quiet. Erin is red. Harry is furry. Harry is red. Furry things are white. If something is red then it is furry. If Anne is blue and Anne is furry then Anne is nice. All cold, blue things are nice. Nice, blue things are red. If something is blue and white then it is quiet. If something is furry and not nice then it is quiet. If Anne is quiet and Anne is red then Anne is white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Anne is blue and Anne is furry then Anne is nice.
((("Anne" "is" "blue" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "nice" "+"))
All cold, blue things are nice.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Nice, blue things are red.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is blue and white then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is furry and not nice then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If Anne is quiet and Anne is red then Anne is white.
((("Anne" "is" "quiet" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "white" "+"))
Erin is nice.
True
1
proof
[(triple6)]
("Erin" "is" "nice" "+")
triple6
Harry is not furry.
False
1
inv-proof
[(triple9 OR ((triple10) -> rule2))]
("Harry" "is" "furry" "-")
triple9
((triple10) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
True
2
proof
[(((triple9) -> rule1) OR ((((triple10) -> rule2)) -> rule1))]
("Harry" "is" "white" "+")
((triple9) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Erin is not furry.
False
2
inv-proof
[(((triple8) -> rule2))]
("Erin" "is" "furry" "-")
((triple8) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
True
3
proof
[(((((triple8) -> rule2)) -> rule1))]
("Erin" "is" "white" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule1))]
("Erin" "is" "white" "-")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is furry.
True
6
proof
[(((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2))]
("Anne" "is" "furry" "+")
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not furry.
False
6
inv-proof
[(((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2))]
("Anne" "is" "furry" "-")
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
True
7
proof
[(((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is not white.
False
7
inv-proof
[(((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is quiet.
True
9
proof
[(((triple1 ((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1)) -> rule6))]
("Anne" "is" "quiet" "+")
((triple1 ((((((((triple2 triple1) -> (rule4 % int5)) triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Anne is not quiet.
False
9
inv-proof
[(((triple1 ((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1)) -> rule6))]
("Anne" "is" "quiet" "-")
((triple1 ((((((((triple2 triple1) -> (rule4 % int5)) triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "nice" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Dave is red.[(triple3)] Dave is white.[(triple4 OR ((((triple3) -> rule2)) -> rule1))] Erin is cold.[(triple5)] Erin is nice.[(triple6)] Erin is quiet.[(triple7)] Erin is red.[(triple8)] Harry is furry.[(triple9 OR ((triple10) -> rule2))] Harry is red.[(triple10)] @1: Anne is nice.[(((triple2 triple1) -> rule4))] Dave is furry.[(((triple3) -> rule2))] Erin is furry.[(((triple8) -> rule2))] Harry is white.[(((triple9) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] @2: Anne is red.[(((((triple2 triple1) -> rule4) triple1) -> rule5))] Erin is white.[(((((triple8) -> rule2)) -> rule1))] @3: Anne is furry.[(((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2))] @4: Anne is white.[(((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1))] @5: Anne is quiet.[(((triple1 ((((((((triple2 triple1) -> rule4) triple1) -> rule5)) -> rule2)) -> rule1)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple10) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple8) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple9) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple2 triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple2 triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((((triple2 triple1) -> (rule4 % int4)) triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((((((((triple2 triple1) -> (rule4 % int5)) triple1) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5