Anne is big. Anne is nice. Anne is smart. Charlie is big. Charlie is furry. Charlie is red. Dave is not big. Dave is furry. Dave is kind. Dave is nice. Dave is not red. Dave is not round. Dave is not smart. Erin is not kind. Erin is red. Smart people are round. If someone is red and not nice then they are big. If someone is smart and not big then they are furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not round.
("Dave" "is" "round" "-")
Dave is not smart.
("Dave" "is" "smart" "-")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is red.
("Erin" "is" "red" "+")
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is red and not nice then they are big.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "+"))
If someone is smart and not big then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
Dave is not red.
True
1
proof
[(triple11)]
("Dave" "is" "red" "-")
triple11
Dave is round.
False
1
inv-proof
[(triple12)]
("Dave" "is" "round" "+")
triple12
Anne is round.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "round" "+")
((triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "round" "-")
((triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3)] Charlie is big.[(triple4)] Charlie is furry.[(triple5)] Charlie is red.[(triple6)] Dave is furry.[(triple8)] Dave is kind.[(triple9)] Dave is nice.[(triple10)] Dave is not big.[(triple7)] Dave is not red.[(triple11)] Dave is not round.[(triple12)] Dave is not smart.[(triple13)] Erin is not kind.[(triple14)] Erin is red.[(triple15)] @1: Anne is round.[(((triple3) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not big.
("Dave" "is" "big" "-")
triple7
Dave is not red.
("Dave" "is" "red" "-")
triple11
Dave is not round.
("Dave" "is" "round" "-")
triple12
Dave is not smart.
("Dave" "is" "smart" "-")
triple13
Erin is not kind.
("Erin" "is" "kind" "-")
triple14
Erin is red.
("Erin" "is" "red" "+")
triple15
Anne is round.
("Anne" "is" "round" "+")
((triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1