Bob is round. Dave is young. Gary is furry. Red things are kind. All furry things are red. If something is red and kind then it is green.
Bob is round.
("Bob" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All furry things are red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is red and kind then it is green.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Gary is red.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "red" "+")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
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 kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not green.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule3))]
("Gary" "is" "green" "-")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "kind" "+")
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is round.[(triple1)] Dave is young.[(triple2)] Gary is furry.[(triple3)] @1: Gary is red.[(((triple3) -> rule2))] @2: Gary is kind.[(((((triple3) -> rule2)) -> rule1))] @3: Gary is green.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule1)) -> rule3))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3