Anne is furry. Anne is green. Anne is red. Bob is big. Bob is blue. Bob is red. Dave is big. Dave is kind. Dave is red. Erin is blue. Erin is kind. Erin is round. If Anne is big then Anne is not kind. If something is blue and not green then it is round. Red things are big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
If Anne is big then Anne is not kind.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "kind" "-"))
If something is blue and not green then it is round.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "round" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Erin is kind.
True
1
proof
[(triple11)]
("Erin" "is" "kind" "+")
triple11
Erin is not round.
False
1
inv-proof
[(triple12)]
("Erin" "is" "round" "-")
triple12
Anne is big.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "big" "+")
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Anne" "is" "big" "-")
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not kind.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Anne" "is" "kind" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Anne" "is" "kind" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is red.[(triple3)] Bob is big.[(triple4 OR ((triple6) -> rule3))] Bob is blue.[(triple5)] Bob is red.[(triple6)] Dave is big.[(triple7 OR ((triple9) -> rule3))] Dave is kind.[(triple8)] Dave is red.[(triple9)] Erin is blue.[(triple10)] Erin is kind.[(triple11)] Erin is round.[(triple12)] @1: Anne is big.[(((triple3) -> rule3))] @2: Anne is not kind.[(((((triple3) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
triple4
((triple6) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Dave is big.
("Dave" "is" "big" "+")
triple7
((triple9) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Erin is blue.
("Erin" "is" "blue" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2