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