Anne is green. Anne is not round. Dave is green. Erin is big. Erin is cold. Erin is not white. Harry is rough. Rough things are not round. If something is kind and not white then it is round. All white, cold things are big. All green things are not cold. If something is cold and not round then it is green. If Anne is cold then Anne is green.
Anne is green.
("Anne" "is" "green" "+")
Anne is not round.
("Anne" "is" "round" "-")
Dave is green.
("Dave" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not white.
("Erin" "is" "white" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Rough things are not round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
If something is kind and not white then it is round.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "+"))
All white, cold things are big.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All green things are not cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "-"))
If something is cold and not round then it is green.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "is" "green" "+"))
If Anne is cold then Anne is green.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "green" "+"))
Erin is cold.
True
1
proof
[(triple5)]
("Erin" "is" "cold" "+")
triple5
Erin is white.
False
1
inv-proof
[(triple6)]
("Erin" "is" "white" "+")
triple6
Dave is not cold.
True
2
proof
[(((triple3) -> rule4))]
("Dave" "is" "cold" "-")
((triple3) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Anne is cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "green" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is not round.[(triple2)] Dave is green.[(triple3)] Erin is big.[(triple4)] Erin is cold.[(triple5)] Erin is not white.[(triple6)] Harry is rough.[(triple7)] @1: Anne is not cold.[(((triple1) -> rule4))] Dave is not cold.[(((triple3) -> rule4))] Harry is not round.[(((triple7) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not round.
("Anne" "is" "round" "-")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is not white.
("Erin" "is" "white" "-")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Dave is not cold.
("Dave" "is" "cold" "-")
((triple3) -> (rule4 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Harry is not round.
("Harry" "is" "round" "-")
((triple7) -> (rule1 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1