Anne is red. Anne is white. Charlie is red. Erin is red. Erin is rough. Erin is white. Fiona is white. If Charlie is rough and Charlie is white then Charlie is green. If someone is furry then they are big. All white, kind people are green. All white people are kind. Kind, big people are rough. All green people are furry.
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Charlie is rough and Charlie is white then Charlie is green.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "green" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All white, kind people are green.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All white people are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
Kind, big people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Charlie is red.
True
1
proof
[(triple3)]
("Charlie" "is" "red" "+")
triple3
Fiona is not white.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "white" "-")
triple7
Erin is kind.
True
2
proof
[(((triple6) -> rule4))]
("Erin" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple7) -> rule4))]
("Fiona" "is" "kind" "-")
((triple7) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Erin is green.
True
4
proof
[(((triple6 ((triple6) -> rule4)) -> rule3))]
("Erin" "is" "green" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((triple7 ((triple7) -> rule4)) -> rule3))]
("Fiona" "is" "green" "-")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Erin is furry.
True
5
proof
[(((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "furry" "+")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not furry.
False
5
inv-proof
[(((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "furry" "-")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is big.
True
6
proof
[(((((((triple7 ((triple7) -> rule4)) -> rule3)) -> rule6)) -> rule2))]
("Fiona" "is" "big" "+")
((((((triple7 ((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Erin is not big.
False
6
inv-proof
[(((((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6)) -> rule2))]
("Erin" "is" "big" "-")
((((((triple6 ((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Anne is rough.
True
9
proof
[(((((triple2) -> rule4) ((((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple2) -> (rule4 % int5)) ((((((triple2 ((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5
Fiona is not rough.
False
9
inv-proof
[(((((triple7) -> rule4) ((((((triple7 ((triple7) -> rule4)) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
("Fiona" "is" "rough" "-")
((((triple7) -> (rule4 % int5)) ((((((triple7 ((triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not big.
Unknown
inv-rconc
[@3: Charlie is big.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Anne is red.[(triple1)] Anne is white.[(triple2)] Charlie is red.[(triple3)] Erin is red.[(triple4)] Erin is rough.[(triple5 OR ((((triple6) -> rule4) ((((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6)) -> rule2)) -> rule5))] Erin is white.[(triple6)] Fiona is white.[(triple7)] @1: Anne is kind.[(((triple2) -> rule4))] Erin is kind.[(((triple6) -> rule4))] Fiona is kind.[(((triple7) -> rule4))] @2: Anne is green.[(((triple2 ((triple2) -> rule4)) -> rule3))] Erin is green.[(((triple6 ((triple6) -> rule4)) -> rule3))] Fiona is green.[(((triple7 ((triple7) -> rule4)) -> rule3))] @3: Anne is furry.[(((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6))] Erin is furry.[(((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6))] Fiona is furry.[(((((triple7 ((triple7) -> rule4)) -> rule3)) -> rule6))] @4: Anne is big.[(((((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6)) -> rule2))] Erin is big.[(((((((triple6 ((triple6) -> rule4)) -> rule3)) -> rule6)) -> rule2))] Fiona is big.[(((((((triple7 ((triple7) -> rule4)) -> rule3)) -> rule6)) -> rule2))] @5: Anne is rough.[(((((triple2) -> rule4) ((((((triple2 ((triple2) -> rule4)) -> rule3)) -> rule6)) -> rule2)) -> rule5))] Fiona is rough.[(((((triple7) -> rule4) ((((((triple7 ((triple7) -> rule4)) -> rule3)) -> rule6)) -> rule2)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((((triple6) -> (rule4 % int5)) ((((((triple6 ((triple6) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is white.
("Erin" "is" "white" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple7) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple7 ((triple7) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((((triple2 ((triple2) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((((((triple6 ((triple6) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple7 ((triple7) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((triple2) -> (rule4 % int5)) ((((((triple2 ((triple2) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple7) -> (rule4 % int5)) ((((((triple7 ((triple7) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5