Anne is furry. Anne is green. Charlie is green. Charlie is not red. Erin is red. Erin is rough. Gary is green. All nice, smart people are green. If Anne is smart then Anne is nice. Green people are round. If Gary is round then Gary is not nice. If someone is green and not nice then they are not rough. If Erin is green and Erin is not round then Erin is red. All smart, red people are not furry. All round, red people are furry. If someone is round and not rough then they are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
All nice, smart people are green.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Anne is smart then Anne is nice.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "nice" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Gary is round then Gary is not nice.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "nice" "-"))
If someone is green and not nice then they are not rough.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "rough" "-"))
If Erin is green and Erin is not round then Erin is red.
((("Erin" "is" "green" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "red" "+"))
All smart, red people are not furry.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "-"))
All round, red people are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and not rough then they are red.
((("someone" "is" "round" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Gary is not green.
False
1
inv-proof
[(triple7)]
("Gary" "is" "green" "-")
triple7
Gary is round.
True
2
proof
[(((triple7) -> rule3))]
("Gary" "is" "round" "+")
((triple7) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("Charlie" "is" "round" "-")
((triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is not nice.
True
3
proof
[(((((triple7) -> rule3)) -> rule4))]
("Gary" "is" "nice" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is nice.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule4))]
("Gary" "is" "nice" "+")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not rough.
True
5
proof
[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5))]
("Gary" "is" "rough" "-")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5))]
("Gary" "is" "rough" "+")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
True
8
proof
[(((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9))]
("Gary" "is" "red" "+")
((((triple7) -> (rule3 % int4)) ((triple7 ((((triple7) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not red.
False
8
inv-proof
[(((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9))]
("Gary" "is" "red" "-")
((((triple7) -> (rule3 % int4)) ((triple7 ((((triple7) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is furry.
True
11
proof
[(((((triple7) -> rule3) ((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9)) -> rule8))]
("Gary" "is" "furry" "+")
((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5)) ((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
int3
Gary is not nice.
("Gary" "is" "nice" "-")
int4
Gary is round.
("Gary" "is" "round" "+")
int5
Gary is not furry.
False
11
inv-proof
[(((((triple7) -> rule3) ((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9)) -> rule8))]
("Gary" "is" "furry" "-")
((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5)) ((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
int3
Gary is not nice.
("Gary" "is" "nice" "-")
int4
Gary is round.
("Gary" "is" "round" "+")
int5
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is furry.
Unknown
rconc
[@3: Erin is furry.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule1 <- FAIL)]]
("Erin" "is" "furry" "+")
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Anne" "is" "red" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Charlie is green.[(triple3)] Charlie is not red.[(triple4)] Erin is red.[(triple5)] Erin is rough.[(triple6)] Gary is green.[(triple7)] @1: Anne is round.[(((triple2) -> rule3))] Charlie is round.[(((triple3) -> rule3))] Gary is round.[(((triple7) -> rule3))] @2: Gary is not nice.[(((((triple7) -> rule3)) -> rule4))] @3: Gary is not rough.[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5))] @4: Gary is red.[(((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9))] @5: Gary is furry.[(((((triple7) -> rule3) ((((triple7) -> rule3) ((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule5)) -> rule9)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple7) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple7) -> (rule3 % int4)) ((triple7 ((((triple7) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
((((triple7) -> (rule3 % int5)) ((((triple7) -> (rule3 % int5)) ((triple7 ((((triple7) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not rough.
("Gary" "is" "rough" "-")
int3
Gary is not nice.
("Gary" "is" "nice" "-")
int4
Gary is round.
("Gary" "is" "round" "+")
int5