Anne is big. Anne is blue. Anne is cold. Anne is green. Anne is nice. Dave is cold. Dave is white. Nice, blue things are cold. Cold things are white. All cold, nice things are blue. If something is blue and nice then it is big. Big, white things are blue. All cold things are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Nice, blue things are cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All cold, nice things are blue.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is blue and nice then it is big.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Big, white things are blue.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Anne is cold.
True
1
proof
[(triple3 OR ((triple5 triple2) -> rule1))]
("Anne" "is" "cold" "+")
triple3
((triple5 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
1
inv-proof
[(triple3 OR ((triple5 triple2) -> rule1))]
("Anne" "is" "cold" "-")
triple3
((triple5 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
True
2
proof
[(((triple3) -> rule2) OR ((((triple5 triple2) -> rule1)) -> rule2))]
("Anne" "is" "white" "+")
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is not furry.
False
2
inv-proof
[(((triple6) -> rule6))]
("Dave" "is" "furry" "-")
((triple6) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is blue.
Unknown
rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Dave" "is" "blue" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is big.[(triple1 OR ((triple2 triple5) -> rule4) OR ((((triple3 triple5) -> rule3) triple5) -> rule4))] Anne is blue.[(triple2 OR ((triple3 triple5) -> rule3) OR ((triple1 ((triple3) -> rule2)) -> rule5))] Anne is cold.[(triple3 OR ((triple5 triple2) -> rule1))] Anne is green.[(triple4)] Anne is nice.[(triple5)] Dave is cold.[(triple6)] Dave is white.[(triple7 OR ((triple6) -> rule2))] @1: Anne is furry.[(((triple3) -> rule6) OR ((((triple5 triple2) -> rule1)) -> rule6))] Anne is white.[(((triple3) -> rule2) OR ((((triple5 triple2) -> rule1)) -> rule2))] Dave is furry.[(((triple6) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2 triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple3 triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple3 triple5) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple1 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple5 triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
((triple6) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple3) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple5 triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5 triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple6) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1