Anne is nice. Anne is round. Anne is white. Dave is furry. Dave is round. Dave is smart. Erin is furry. Erin is round. Erin is smart. Fiona is nice. Fiona is not round. Fiona is white. If Fiona is furry and Fiona is smart then Fiona is not nice. If someone is round and not big then they are not white. Furry people are not green. If Anne is not smart then Anne is not round. All big people are not round. All round people are furry.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is furry and Fiona is smart then Fiona is not nice.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "nice" "-"))
If someone is round and not big then they are not white.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "-"))
Furry people are not green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "-"))
If Anne is not smart then Anne is not round.
((("Anne" "is" "smart" "~")) -> ("Anne" "is" "round" "-"))
All big people are not round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "-"))
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Anne is round.
True
1
proof
[(triple2)]
("Anne" "is" "round" "+")
triple2
Erin is not round.
False
1
inv-proof
[(triple8)]
("Erin" "is" "round" "-")
triple8
Erin is not green.
True
2
proof
[(((triple7) -> rule3) OR ((((triple8) -> rule6)) -> rule3))]
("Erin" "is" "green" "-")
((triple7) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple8) -> rule6)) -> rule3))]
("Erin" "is" "green" "+")
((triple7) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is not green.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("Anne" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Anne" "is" "green" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "furry" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is nice.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] Dave is furry.[(triple4 OR ((triple5) -> rule6))] Dave is round.[(triple5)] Dave is smart.[(triple6)] Erin is furry.[(triple7 OR ((triple8) -> rule6))] Erin is round.[(triple8)] Erin is smart.[(triple9)] Fiona is nice.[(triple10)] Fiona is not round.[(triple11)] Fiona is white.[(triple12)] @1: Anne is furry.[(((triple2) -> rule6))] Dave is not green.[(((triple4) -> rule3) OR ((((triple5) -> rule6)) -> rule3))] Erin is not green.[(((triple7) -> rule3) OR ((((triple8) -> rule6)) -> rule3))] @2: Anne is not green.[(((((triple2) -> rule6)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple5) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple8) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Fiona is not round.
("Fiona" "is" "round" "-")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple4) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((triple7) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
((((triple8) -> (rule6 % int2))) -> (rule3 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is not green.
("Anne" "is" "green" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2