Charlie is kind. Erin is kind. Gary is white. Kind things are young. All young things are round. If Charlie is round then Charlie is green. All kind, young things are round. All white, furry things are round. If something is red and furry then it is green.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If Charlie is round then Charlie is green.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "green" "+"))
All kind, young things are round.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All white, furry things are round.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If something is red and furry then it is green.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Erin is kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Erin is young.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "young" "-")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
True
3
proof
[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Erin" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule4))]
("Erin" "is" "round" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule3))]
("Charlie" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule3))]
("Charlie" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is kind.[(triple1)] Erin is kind.[(triple2)] Gary is white.[(triple3)] @1: Charlie is young.[(((triple1) -> rule1))] Erin is young.[(((triple2) -> rule1))] @2: Charlie is round.[(((((triple1) -> rule1)) -> rule2) OR ((triple1 ((triple1) -> rule1)) -> rule4))] Erin is round.[(((((triple2) -> rule1)) -> rule2) OR ((triple2 ((triple2) -> rule1)) -> rule4))] @3: Charlie is green.[(((((((triple1) -> rule1)) -> rule2)) -> rule3) OR ((((triple1 ((triple1) -> rule1)) -> rule4)) -> rule3))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3