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