Anne is not green. Erin is green. Gary is green. If Gary is green then Gary is not nice. If Erin is blue then Erin is green. If Anne is big then Anne is smart. If something is big then it is not blue. If Gary is kind and Gary is green then Gary is blue. Green things are smart. If Gary is not nice then Gary is not red. If Gary is kind and Gary is not big then Gary is red.
Anne is not green.
("Anne" "is" "green" "-")
Erin is green.
("Erin" "is" "green" "+")
Gary is green.
("Gary" "is" "green" "+")
If Gary is green then Gary is not nice.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "nice" "-"))
If Erin is blue then Erin is green.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "green" "+"))
If Anne is big then Anne is smart.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "smart" "+"))
If something is big then it is not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If Gary is kind and Gary is green then Gary is blue.
((("Gary" "is" "kind" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "blue" "+"))
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Gary is not nice then Gary is not red.
((("Gary" "is" "nice" "~")) -> ("Gary" "is" "red" "-"))
If Gary is kind and Gary is not big then Gary is red.
((("Gary" "is" "kind" "+") ("Gary" "is" "big" "~")) -> ("Gary" "is" "red" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Gary is smart.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is not red.
True
3
proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "red" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is red.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule7))]
("Gary" "is" "red" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is not green.[(triple1)] Erin is green.[(triple2)] Gary is green.[(triple3)] @1: Erin is smart.[(((triple2) -> rule6))] Gary is not nice.[(((triple3) -> rule1))] Gary is smart.[(((triple3) -> rule6))] @2: Gary is not red.[(((((triple3) -> rule1)) -> rule7))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2