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