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