Anne is big. Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is not red. Anne is round. Dave is cold. Dave is not furry. Dave is red. If someone is round and not red then they are furry. If Anne is big then Anne is round. All round, furry people are big. All furry people are cold. If someone is red and not nice then they are round. If Dave is not nice then Dave is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is round.
("Anne" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is red.
("Dave" "is" "red" "+")
If someone is round and not red then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "furry" "+"))
If Anne is big then Anne is round.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "round" "+"))
All round, furry people are big.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is red and not nice then they are round.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "+"))
If Dave is not nice then Dave is round.
((("Dave" "is" "nice" "~")) -> ("Dave" "is" "round" "+"))
Anne is furry.
True
1
proof
[(triple4 OR ((triple7 triple6) -> rule1) OR ((((triple1) -> rule2) triple6) -> rule1))]
("Anne" "is" "furry" "+")
triple4
((triple7 triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is furry.
False
1
inv-proof
[(triple9)]
("Dave" "is" "furry" "+")
triple9
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is big.[(triple1 OR ((triple7 triple4) -> rule3) OR ((triple7 ((triple7 triple6) -> rule1)) -> rule3))] Anne is blue.[(triple2)] Anne is cold.[(triple3 OR ((triple4) -> rule4) OR ((((triple7 triple6) -> rule1)) -> rule4) OR ((((((triple1) -> rule2) triple6) -> rule1)) -> rule4))] Anne is furry.[(triple4 OR ((triple7 triple6) -> rule1) OR ((((triple1) -> rule2) triple6) -> rule1))] Anne is nice.[(triple5)] Anne is not red.[(triple6)] Anne is round.[(triple7 OR ((triple1) -> rule2))] Dave is cold.[(triple8)] Dave is not furry.[(triple9)] Dave is red.[(triple10)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple7 triple4) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((triple7 ((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
triple3
((triple4) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple1) -> (rule2 % int3)) triple6) -> (rule1 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple4
((triple7 triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is not red.
("Anne" "is" "red" "-")
triple6
Anne is round.
("Anne" "is" "round" "+")
triple7
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is not furry.
("Dave" "is" "furry" "-")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10