Anne is big. Bob is big. Bob is kind. Bob is not red. Dave is kind. Dave is red. Gary is not quiet. If Anne is blue then Anne is cold. If Gary is red then Gary is kind. If something is quiet then it is not red. If something is big then it is not blue. If something is kind and not blue then it is rough. If something is rough then it is kind.
Anne is big.
("Anne" "is" "big" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not red.
("Bob" "is" "red" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
If Anne is blue then Anne is cold.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
If Gary is red then Gary is kind.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "kind" "+"))
If something is quiet then it is not red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "-"))
If something is big then it is not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something is kind and not blue then it is rough.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Gary is quiet.
False
1
inv-proof
[(triple7)]
("Gary" "is" "quiet" "+")
triple7
Anne is not blue.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Bob is blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is rough.
True
4
proof
[(((triple3 ((triple2) -> rule4)) -> rule5))]
("Bob" "is" "rough" "+")
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Bob is not rough.
False
4
inv-proof
[(((triple3 ((triple2) -> rule4)) -> rule5))]
("Bob" "is" "rough" "-")
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "rough" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Anne is big.[(triple1)] Bob is big.[(triple2)] Bob is kind.[(triple3)] Bob is not red.[(triple4)] Dave is kind.[(triple5)] Dave is red.[(triple6)] Gary is not quiet.[(triple7)] @1: Anne is not blue.[(((triple1) -> rule4))] Bob is not blue.[(((triple2) -> rule4))] @2: Bob is rough.[(((triple3 ((triple2) -> rule4)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not red.
("Bob" "is" "red" "-")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Anne is not blue.
("Anne" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3 ((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
int2