Anne is kind. Anne is not red. Anne is round. Dave is big. Dave is furry. Dave is green. Dave is not red. Dave is round. Dave is not smart. Fiona is smart. If someone is kind then they are not green. If Dave is green and Dave is not kind then Dave is round. If someone is round and not kind then they are furry. If someone is green then they are furry. If Fiona is red then Fiona is furry. If Anne is big and Anne is round then Anne is smart. If someone is green and not round then they are big. Kind people are big.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is round.
("Anne" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
If someone is kind then they are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
If Dave is green and Dave is not kind then Dave is round.
((("Dave" "is" "green" "+") ("Dave" "is" "kind" "~")) -> ("Dave" "is" "round" "+"))
If someone is round and not kind then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "furry" "+"))
If someone is green then they are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Fiona is red then Fiona is furry.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "furry" "+"))
If Anne is big and Anne is round then Anne is smart.
((("Anne" "is" "big" "+") ("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
If someone is green and not round then they are big.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Anne is red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "+")
triple2
Anne is not green.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "big" "-")
((triple1) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is smart.
True
4
proof
[(((((triple1) -> rule8) triple3) -> rule6))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule8 % int2)) triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((((triple1) -> rule8) triple3) -> rule6))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule8 % int2)) triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "furry" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is not red.[(triple2)] Anne is round.[(triple3)] Dave is big.[(triple4)] Dave is furry.[(triple5 OR ((triple6) -> rule4))] Dave is green.[(triple6)] Dave is not red.[(triple7)] Dave is not smart.[(triple9)] Dave is round.[(triple8)] Fiona is smart.[(triple10)] @1: Anne is big.[(((triple1) -> rule8))] Anne is not green.[(((triple1) -> rule1))] @2: Anne is smart.[(((((triple1) -> rule8) triple3) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
((triple6) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is not red.
("Dave" "is" "red" "-")
triple7
Dave is not smart.
("Dave" "is" "smart" "-")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not green.
("Anne" "is" "green" "-")
((triple1) -> (rule1 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule8 % int2)) triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2