Anne is furry. Anne is kind. Dave is white. Erin is big. Erin is not furry. Erin is rough. Gary is green. Green things are rough. All white things are red. Rough, big things are red. Green, big things are red. If something is kind then it is white. If something is red then it is big. If Anne is big and Anne is kind then Anne is green. If something is kind and not white then it is furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Rough, big things are red.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
Green, big things are red.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Anne is big and Anne is kind then Anne is green.
((("Anne" "is" "big" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "green" "+"))
If something is kind and not white then it is furry.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "furry" "+"))
Gary is green.
True
1
proof
[(triple7)]
("Gary" "is" "green" "+")
triple7
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Gary is rough.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple2) -> rule5))]
("Anne" "is" "white" "-")
((triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Anne" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Anne" "is" "red" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "big" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not big.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "big" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
True
6
proof
[(((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7))]
("Anne" "is" "green" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is not green.
False
6
inv-proof
[(((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7))]
("Anne" "is" "green" "-")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is rough.
True
7
proof
[(((((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7)) -> rule1))]
("Anne" "is" "rough" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule7 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Anne is not rough.
False
7
inv-proof
[(((((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7)) -> rule1))]
("Anne" "is" "rough" "-")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule7 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "furry" "-")
Gary is red.
Unknown
rconc
[@4: Gary is red.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule2 <- rule5 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "furry" "+")
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Gary is big.
Unknown
rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- FAIL)]]
("Gary" "is" "big" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Dave is white.[(triple3)] Erin is big.[(triple4)] Erin is not furry.[(triple5)] Erin is rough.[(triple6)] Gary is green.[(triple7)] @1: Anne is white.[(((triple2) -> rule5))] Dave is red.[(((triple3) -> rule2))] Erin is red.[(((triple6 triple4) -> rule3))] Gary is rough.[(((triple7) -> rule1))] @2: Anne is red.[(((((triple2) -> rule5)) -> rule2))] Dave is big.[(((((triple3) -> rule2)) -> rule6))] @3: Anne is big.[(((((((triple2) -> rule5)) -> rule2)) -> rule6))] @4: Anne is green.[(((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7))] @5: Anne is rough.[(((((((((((triple2) -> rule5)) -> rule2)) -> rule6) triple2) -> rule7)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is not furry.
("Erin" "is" "furry" "-")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple6 triple4) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) triple2) -> (rule7 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
int5