Anne is green. Anne is nice. Anne is not red. Anne is not round. Dave is red. Dave is round. Dave is white. Gary is cold. Gary is nice. Gary is red. Gary is smart. Gary is white. If Dave is cold then Dave is white. If something is cold and white then it is green. Cold things are red. If Anne is nice and Anne is not smart then Anne is round. If Dave is white and Dave is smart then Dave is nice. If something is cold then it is white. If something is smart and not white then it is not round. If Dave is cold and Dave is not round then Dave is not green.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is not round.
("Anne" "is" "round" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is cold then Dave is white.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
If something is cold and white then it is green.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If Anne is nice and Anne is not smart then Anne is round.
((("Anne" "is" "nice" "+") ("Anne" "is" "smart" "~")) -> ("Anne" "is" "round" "+"))
If Dave is white and Dave is smart then Dave is nice.
((("Dave" "is" "white" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "nice" "+"))
If something is cold then it is white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is smart and not white then it is not round.
((("something" "is" "smart" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "-"))
If Dave is cold and Dave is not round then Dave is not green.
((("Dave" "is" "cold" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "green" "-"))
Gary is nice.
True
1
proof
[(triple9)]
("Gary" "is" "nice" "+")
triple9
Gary is not smart.
False
1
inv-proof
[(triple11)]
("Gary" "is" "smart" "-")
triple11
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2)] Anne is not red.[(triple3)] Anne is not round.[(triple4)] Dave is red.[(triple5)] Dave is round.[(triple6)] Dave is white.[(triple7)] Gary is cold.[(triple8)] Gary is nice.[(triple9)] Gary is red.[(triple10 OR ((triple8) -> rule3))] Gary is smart.[(triple11)] Gary is white.[(triple12 OR ((triple8) -> rule6))] @1: Gary is green.[(((triple8 triple12) -> rule2) OR ((triple8 ((triple8) -> rule6)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not red.
("Anne" "is" "red" "-")
triple3
Anne is not round.
("Anne" "is" "round" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
((triple8) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
((triple8) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple8 triple12) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple8 ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2