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