Anne is rough. Dave is big. Gary is rough. If Dave is rough and Dave is cold then Dave is big. If Anne is rough then Anne is not cold. If something is smart and not rough then it is big. If something is big then it is not smart. If something is big then it is cold. If something is smart and not big then it is not red.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Dave is rough and Dave is cold then Dave is big.
((("Dave" "is" "rough" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "big" "+"))
If Anne is rough then Anne is not cold.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "-"))
If something is smart and not rough then it is big.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
If something is big then it is not smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "-"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is smart and not big then it is not red.
((("something" "is" "smart" "+") ("something" "is" "big" "~")) -> ("something" "is" "red" "-"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is not smart.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is rough.[(triple1)] Dave is big.[(triple2)] Gary is rough.[(triple3)] @1: Anne is not cold.[(((triple1) -> rule2))] Dave is cold.[(((triple2) -> rule5))] Dave is not smart.[(((triple2) -> rule4))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Anne is not cold.
("Anne" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple2) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not smart.
("Dave" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1