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