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