Anne is red. Dave is green. Gary is smart. If something is kind then it is red. If Gary is smart then Gary is red. If something is red then it is not kind. If Gary is red then Gary is green. If something is green and red then it is young. If something is smart and not kind then it is young. Young things are furry. If something is smart and not red then it is furry.
Anne is red.
("Anne" "is" "red" "+")
Dave is green.
("Dave" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Gary is smart then Gary is red.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "red" "+"))
If something is red then it is not kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
If Gary is red then Gary is green.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "green" "+"))
If something is green and red then it is young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is smart and not kind then it is young.
((("something" "is" "smart" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is smart and not red then it is furry.
((("something" "is" "smart" "+") ("something" "is" "red" "~")) -> ("something" "is" "furry" "+"))
Gary is smart.
True
1
proof
[(triple3)]
("Gary" "is" "smart" "+")
triple3
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Anne is not kind.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "red" "-")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("Gary" "is" "green" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
True
5
proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule4) ((triple3) -> rule2)) -> rule5))]
("Gary" "is" "young" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2)) ((triple3) -> (rule2 % int3))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not young.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule4) ((triple3) -> rule2)) -> rule5))]
("Gary" "is" "young" "-")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2)) ((triple3) -> (rule2 % int3))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("Anne" "is" "furry" "-")
Dave is furry.
Unknown
rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is red.[(triple1)] Dave is green.[(triple2)] Gary is smart.[(triple3)] @1: Anne is not kind.[(((triple1) -> rule3))] Gary is red.[(((triple3) -> rule2))] @2: Gary is green.[(((((triple3) -> rule2)) -> rule4))] Gary is not kind.[(((((triple3) -> rule2)) -> rule3))] @3: Gary is young.[(((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule4) ((triple3) -> rule2)) -> rule5))] @4: Gary is furry.[(((((triple3 ((((triple3) -> rule2)) -> rule3)) -> rule6)) -> rule7) OR ((((((((triple3) -> rule2)) -> rule4) ((triple3) -> rule2)) -> rule5)) -> rule7))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is not kind.
("Gary" "is" "kind" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2)) ((triple3) -> (rule2 % int3))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3 ((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not kind.
("Gary" "is" "kind" "-")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((((triple3) -> (rule2 % int4))) -> (rule4 % int3)) ((triple3) -> (rule2 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4