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