Anne is smart. Erin is not round. Fiona is not round. Harry is not round. If Fiona is smart and Fiona is green then Fiona is not furry. White people are round. If someone is green and nice then they are round. If someone is nice and smart then they are blue. Blue people are nice. If someone is smart then they are nice.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is not round.
("Erin" "is" "round" "-")
Fiona is not round.
("Fiona" "is" "round" "-")
Harry is not round.
("Harry" "is" "round" "-")
If Fiona is smart and Fiona is green then Fiona is not furry.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "furry" "-"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is green and nice then they are round.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and smart then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Erin is round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Anne is nice.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule4))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not blue.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule4))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is smart.[(triple1)] Erin is not round.[(triple2)] Fiona is not round.[(triple3)] Harry is not round.[(triple4)] @1: Anne is nice.[(((triple1) -> rule6))] @2: Anne is blue.[(((((triple1) -> rule6) triple1) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is not round.
("Erin" "is" "round" "-")
triple2
Fiona is not round.
("Fiona" "is" "round" "-")
triple3
Harry is not round.
("Harry" "is" "round" "-")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2