Anne is big. Anne is blue. Anne is not furry. Anne is quiet. Anne is rough. Anne is smart. Erin is big. Erin is blue. Erin is not furry. Erin is not quiet. Erin is red. Erin is rough. Erin is smart. Gary is not furry. Gary is quiet. Gary is red. All blue things are smart. If something is furry then it is smart. If Gary is big then Gary is quiet. All red, furry things are not big. If something is furry then it is not red. Smart things are red. All blue things are rough. If something is furry and not red then it is quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If Gary is big then Gary is quiet.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "quiet" "+"))
All red, furry things are not big.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "-"))
If something is furry then it is not red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "-"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is furry and not red then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "red" "~")) -> ("something" "is" "quiet" "+"))
Gary is quiet.
True
1
proof
[(triple15)]
("Gary" "is" "quiet" "+")
triple15
Erin is furry.
False
1
inv-proof
[(triple9)]
("Erin" "is" "furry" "+")
triple9
Anne is red.
True
2
proof
[(((triple6) -> rule6) OR ((((triple2) -> rule1)) -> rule6))]
("Anne" "is" "red" "+")
((triple6) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
False
2
inv-proof
[(((triple6) -> rule6) OR ((((triple2) -> rule1)) -> rule6))]
("Anne" "is" "red" "-")
((triple6) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is not furry.[(triple3)] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple2) -> rule7))] Anne is smart.[(triple6 OR ((triple2) -> rule1))] Erin is big.[(triple7)] Erin is blue.[(triple8)] Erin is not furry.[(triple9)] Erin is not quiet.[(triple10)] Erin is red.[(triple11 OR ((triple13) -> rule6) OR ((((triple8) -> rule1)) -> rule6))] Erin is rough.[(triple12 OR ((triple8) -> rule7))] Erin is smart.[(triple13 OR ((triple8) -> rule1))] Gary is not furry.[(triple14)] Gary is quiet.[(triple15)] Gary is red.[(triple16)] @1: Anne is red.[(((triple6) -> rule6) OR ((((triple2) -> rule1)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is not furry.
("Anne" "is" "furry" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple2) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is not furry.
("Erin" "is" "furry" "-")
triple9
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple10
Erin is red.
("Erin" "is" "red" "+")
triple11
((triple13) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple12
((triple8) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple13
((triple8) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
triple14
Gary is quiet.
("Gary" "is" "quiet" "+")
triple15
Gary is red.
("Gary" "is" "red" "+")
triple16
Anne is red.
("Anne" "is" "red" "+")
((triple6) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2