Anne is green. Anne is red. Bob is big. Bob is cold. Bob is not green. Bob is smart. Bob is white. If someone is white and not cold then they are not red. If someone is green then they are white. If Bob is green and Bob is cold then Bob is big. If Anne is green then Anne is red. If someone is red and cold then they are not green. If Anne is big and Anne is not red then Anne is smart.
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is white and not cold then they are not red.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "-"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If Bob is green and Bob is cold then Bob is big.
((("Bob" "is" "green" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "big" "+"))
If Anne is green then Anne is red.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "red" "+"))
If someone is red and cold then they are not green.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "-"))
If Anne is big and Anne is not red then Anne is smart.
((("Anne" "is" "big" "+") ("Anne" "is" "red" "~")) -> ("Anne" "is" "smart" "+"))
Anne is red.
True
1
proof
[(triple2 OR ((triple1) -> rule4))]
("Anne" "is" "red" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
Anne is white.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "white" "-")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "smart" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is green.[(triple1)] Anne is red.[(triple2 OR ((triple1) -> rule4))] Bob is big.[(triple3)] Bob is cold.[(triple4)] Bob is not green.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7)] @1: Anne is white.[(((triple1) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1