Anne is furry. Anne is quiet. Erin is blue. Erin is furry. Erin is quiet. Gary is big. Gary is blue. Gary is furry. Gary is nice. Gary is quiet. Gary is round. Harry is red. Big, red things are furry. If something is big and blue then it is nice. All quiet things are furry. All furry things are round. Big, furry things are blue. All nice things are quiet. Red things are big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Big, red things are furry.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is big and blue then it is nice.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Big, furry things are blue.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Gary is nice.
True
1
proof
[(triple9 OR ((triple6 triple7) -> rule2) OR ((triple6 ((triple6 triple8) -> rule5)) -> rule2) OR ((triple6 ((triple6 ((triple10) -> rule3)) -> rule5)) -> rule2))]
("Gary" "is" "nice" "+")
triple9
((triple6 triple7) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple6 ((triple6 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple6 ((triple6 ((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not round.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule4) OR ((((triple10) -> rule3)) -> rule4) OR ((((((triple9) -> rule6)) -> rule3)) -> rule4) OR ((((((((triple6 triple7) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("Gary" "is" "round" "-")
triple11
((triple8) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((((triple6 triple7) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Anne is round.
True
2
proof
[(((triple1) -> rule4) OR ((((triple2) -> rule3)) -> rule4))]
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Harry is not big.
False
2
inv-proof
[(((triple12) -> rule7))]
("Harry" "is" "big" "-")
((triple12) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
True
4
proof
[(((((triple12) -> rule7) triple12) -> rule1))]
("Harry" "is" "furry" "+")
((((triple12) -> (rule7 % int2)) triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple12) -> rule7) triple12) -> rule1))]
("Harry" "is" "furry" "-")
((((triple12) -> (rule7 % int2)) triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
True
7
proof
[(((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5))]
("Harry" "is" "blue" "+")
((((triple12) -> (rule7 % int3)) ((((triple12) -> (rule7 % int3)) triple12) -> (rule1 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple12) -> rule7) triple12) -> rule1)) -> rule4))]
("Harry" "is" "round" "-")
((((((triple12) -> (rule7 % int3)) triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
True
10
proof
[(((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is not nice.
False
10
inv-proof
[(((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is quiet.
True
11
proof
[(((((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2)) -> rule6))]
("Harry" "is" "quiet" "+")
((((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) triple12) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Harry is not quiet.
False
11
inv-proof
[(((((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2)) -> rule6))]
("Harry" "is" "quiet" "-")
((((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) triple12) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Erin" "is" "nice" "-")
Anne is blue.
Unknown
rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Anne" "is" "blue" "+")
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Anne" "is" "nice" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is furry.[(triple1 OR ((triple2) -> rule3))] Anne is quiet.[(triple2)] Erin is blue.[(triple3)] Erin is furry.[(triple4 OR ((triple5) -> rule3))] Erin is quiet.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7 OR ((triple6 triple8) -> rule5) OR ((triple6 ((triple10) -> rule3)) -> rule5) OR ((triple6 ((((triple9) -> rule6)) -> rule3)) -> rule5))] Gary is furry.[(triple8 OR ((triple10) -> rule3) OR ((((triple9) -> rule6)) -> rule3) OR ((((((triple6 triple7) -> rule2)) -> rule6)) -> rule3))] Gary is nice.[(triple9 OR ((triple6 triple7) -> rule2) OR ((triple6 ((triple6 triple8) -> rule5)) -> rule2) OR ((triple6 ((triple6 ((triple10) -> rule3)) -> rule5)) -> rule2))] Gary is quiet.[(triple10 OR ((triple9) -> rule6) OR ((((triple6 triple7) -> rule2)) -> rule6) OR ((((triple6 ((triple6 triple8) -> rule5)) -> rule2)) -> rule6))] Gary is round.[(triple11 OR ((triple8) -> rule4) OR ((((triple10) -> rule3)) -> rule4) OR ((((((triple9) -> rule6)) -> rule3)) -> rule4) OR ((((((((triple6 triple7) -> rule2)) -> rule6)) -> rule3)) -> rule4))] Harry is red.[(triple12)] @1: Anne is round.[(((triple1) -> rule4) OR ((((triple2) -> rule3)) -> rule4))] Erin is round.[(((triple4) -> rule4) OR ((((triple5) -> rule3)) -> rule4))] Harry is big.[(((triple12) -> rule7))] @2: Harry is furry.[(((((triple12) -> rule7) triple12) -> rule1))] @3: Harry is blue.[(((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5))] Harry is round.[(((((((triple12) -> rule7) triple12) -> rule1)) -> rule4))] @4: Harry is nice.[(((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2))] @5: Harry is quiet.[(((((((triple12) -> rule7) ((((triple12) -> rule7) ((((triple12) -> rule7) triple12) -> rule1)) -> rule5)) -> rule2)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
((triple5) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((triple6 triple8) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple6 ((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple6 ((((triple9) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((triple10) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple6 triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple6 triple7) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple6 ((triple6 triple8) -> (rule5 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple6 ((triple6 ((triple10) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
((triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple6 triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple6 ((triple6 triple8) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple11
((triple8) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((((triple6 triple7) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple4) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple12) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple12) -> (rule7 % int2)) triple12) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple12) -> (rule7 % int3)) ((((triple12) -> (rule7 % int3)) triple12) -> (rule1 % int2))) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((((triple12) -> (rule7 % int3)) triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) ((((triple12) -> (rule7 % int4)) triple12) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) ((((triple12) -> (rule7 % int5)) triple12) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5