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