Anne is blue. Dave is furry. Gary is not rough. If Gary is blue then Gary is not big. All kind people are not green. If Dave is furry then Dave is big. All furry, blue people are young. If someone is big then they are not kind. If someone is big and not kind then they are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
If Gary is blue then Gary is not big.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "-"))
All kind people are not green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "-"))
If Dave is furry then Dave is big.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "big" "+"))
All furry, blue people are young.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is big then they are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
If someone is big and not kind then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "rough" "+"))
Gary is not rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Dave is big.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule3))]
("Dave" "is" "big" "-")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Dave" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
True
6
proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is blue.[(triple1)] Dave is furry.[(triple2)] Gary is not rough.[(triple3)] @1: Dave is big.[(((triple2) -> rule3))] @2: Dave is not kind.[(((((triple2) -> rule3)) -> rule5))] @3: Dave is rough.[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule5)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
int2
Dave is big.
("Dave" "is" "big" "+")
int3