Anne is furry. Anne is not smart. Anne is white. Dave is nice. Dave is round. Dave is not white. Erin is not blue. Erin is cold. Erin is furry. Erin is not nice. Erin is round. Erin is smart. Erin is white. Gary is blue. Gary is cold. Gary is round. Smart people are white. If Erin is smart then Erin is white. If someone is round then they are furry. All blue people are smart. If someone is nice and not smart then they are not cold. If someone is round then they are cold. Blue, nice people are cold. If someone is round and not smart then they are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is white.
("Anne" "is" "white" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not white.
("Dave" "is" "white" "-")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If Erin is smart then Erin is white.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "+"))
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and not smart then they are not cold.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "cold" "-"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Blue, nice people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and not smart then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "nice" "+"))
Erin is smart.
True
1
proof
[(triple12)]
("Erin" "is" "smart" "+")
triple12
Dave is white.
False
1
inv-proof
[(triple6)]
("Dave" "is" "white" "+")
triple6
Dave is cold.
True
2
proof
[(((triple5) -> rule6))]
("Dave" "is" "cold" "+")
((triple5) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple5) -> rule6))]
("Dave" "is" "cold" "-")
((triple5) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is white.
True
3
proof
[(((((triple14) -> rule4)) -> rule1))]
("Gary" "is" "white" "+")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule1))]
("Gary" "is" "white" "-")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "nice" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "smart" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "nice" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is furry.[(triple1)] Anne is not smart.[(triple2)] Anne is white.[(triple3)] Dave is nice.[(triple4)] Dave is not white.[(triple6)] Dave is round.[(triple5)] Erin is cold.[(triple8 OR ((triple11) -> rule6))] Erin is furry.[(triple9 OR ((triple11) -> rule3))] Erin is not blue.[(triple7)] Erin is not nice.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] Erin is white.[(triple13 OR ((triple12) -> rule1) OR ((triple12) -> rule2))] Gary is blue.[(triple14)] Gary is cold.[(triple15 OR ((triple16) -> rule6))] Gary is round.[(triple16)] @1: Dave is cold.[(((triple5) -> rule6))] Dave is furry.[(((triple5) -> rule3))] Gary is furry.[(((triple16) -> rule3))] Gary is smart.[(((triple14) -> rule4))] @2: Gary is white.[(((((triple14) -> rule4)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not white.
("Dave" "is" "white" "-")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple8
((triple11) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple11) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
triple7
Erin is not nice.
("Erin" "is" "nice" "-")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple12) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple12) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple14
Gary is cold.
("Gary" "is" "cold" "+")
triple15
((triple16) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple16
Dave is cold.
("Dave" "is" "cold" "+")
((triple5) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple16) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple14) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2