Dave is quiet. Erin is kind. Gary is cold. Gary is furry. Gary is green. Harry is furry. Harry is green. Cold, big things are white. Green things are white. All big things are quiet. Cold things are white. Kind things are green. If something is green and cold then it is kind. Quiet things are kind. Kind, white things are furry. All kind, furry things are big.
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Cold, big things are white.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is green and cold then it is kind.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Kind, white things are furry.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
All kind, furry things are big.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
Harry is green.
True
1
proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Gary is white.
True
2
proof
[(((triple3) -> rule4) OR ((triple5) -> rule2) OR ((triple3 ((((triple5 triple3) -> rule6) triple4) -> rule9)) -> rule1))]
("Gary" "is" "white" "+")
((triple3) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple5) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple3 ((((triple5 triple3) -> (rule6 % int3)) triple4) -> (rule9 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is not white.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "white" "-")
((triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("Erin" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("Erin" "is" "white" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Dave is white.
True
4
proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule2))]
("Dave" "is" "white" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Gary is not quiet.
False
6
inv-proof
[(((((((triple5 triple3) -> rule6) triple4) -> rule9)) -> rule3) OR ((((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple3) -> rule4)) -> rule8)) -> rule9)) -> rule3) OR ((((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple5) -> rule2)) -> rule8)) -> rule9)) -> rule3))]
("Gary" "is" "quiet" "-")
((((((triple5 triple3) -> (rule6 % int3)) triple4) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple5 triple3) -> (rule6 % int5)) ((((triple5 triple3) -> (rule6 % int5)) ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
((((((triple5 triple3) -> (rule6 % int5)) ((((triple5 triple3) -> (rule6 % int5)) ((triple5) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Erin is big.
True
7
proof
[(((triple2 ((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))]
("Erin" "is" "big" "+")
((triple2 ((triple2 ((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is not big.
False
7
inv-proof
[(((triple2 ((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))]
("Erin" "is" "big" "-")
((triple2 ((triple2 ((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Dave is big.
True
10
proof
[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule5)) -> rule2)) -> rule8)) -> rule9))]
("Dave" "is" "big" "+")
((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5)) ((((((triple1) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Erin is not quiet.
False
8
inv-proof
[(((((triple2 ((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9)) -> rule3))]
("Erin" "is" "quiet" "-")
((((triple2 ((triple2 ((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Harry is not big.
Unknown
inv-rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule9 <- rule7 <- rule3 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is quiet.
Unknown
rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- rule9 <- rule6 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-rconc
[@4: Harry is kind.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule9 <- rule6 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Dave is quiet.[(triple1)] Erin is kind.[(triple2)] Gary is cold.[(triple3)] Gary is furry.[(triple4 OR ((((triple5 triple3) -> rule6) ((triple3) -> rule4)) -> rule8) OR ((((triple5 triple3) -> rule6) ((triple5) -> rule2)) -> rule8))] Gary is green.[(triple5)] Harry is furry.[(triple6)] Harry is green.[(triple7)] @1: Dave is kind.[(((triple1) -> rule7))] Erin is green.[(((triple2) -> rule5))] Gary is kind.[(((triple5 triple3) -> rule6))] Gary is white.[(((triple3) -> rule4) OR ((triple5) -> rule2) OR ((triple3 ((((triple5 triple3) -> rule6) triple4) -> rule9)) -> rule1))] Harry is white.[(((triple7) -> rule2))] @2: Dave is green.[(((((triple1) -> rule7)) -> rule5))] Erin is white.[(((((triple2) -> rule5)) -> rule2))] Gary is big.[(((((triple5 triple3) -> rule6) triple4) -> rule9) OR ((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple3) -> rule4)) -> rule8)) -> rule9) OR ((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple5) -> rule2)) -> rule8)) -> rule9))] @3: Dave is white.[(((((((triple1) -> rule7)) -> rule5)) -> rule2))] Erin is furry.[(((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8))] Gary is quiet.[(((((((triple5 triple3) -> rule6) triple4) -> rule9)) -> rule3) OR ((((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple3) -> rule4)) -> rule8)) -> rule9)) -> rule3) OR ((((((triple5 triple3) -> rule6) ((((triple5 triple3) -> rule6) ((triple5) -> rule2)) -> rule8)) -> rule9)) -> rule3))] @4: Dave is furry.[(((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule5)) -> rule2)) -> rule8))] Erin is big.[(((triple2 ((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9))] @5: Dave is big.[(((((triple1) -> rule7) ((((triple1) -> rule7) ((((((triple1) -> rule7)) -> rule5)) -> rule2)) -> rule8)) -> rule9))] Erin is quiet.[(((((triple2 ((triple2 ((((triple2) -> rule5)) -> rule2)) -> rule8)) -> rule9)) -> rule3))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
((((triple5 triple3) -> (rule6 % int3)) ((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((triple5 triple3) -> (rule6 % int3)) ((triple5) -> (rule2 % int2))) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Dave is kind.
("Dave" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple5 triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple5) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple3 ((((triple5 triple3) -> (rule6 % int3)) triple4) -> (rule9 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple5 triple3) -> (rule6 % int2)) triple4) -> (rule9 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple5 triple3) -> (rule6 % int4)) ((((triple5 triple3) -> (rule6 % int4)) ((triple3) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((triple5 triple3) -> (rule6 % int4)) ((((triple5 triple3) -> (rule6 % int4)) ((triple5) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple5 triple3) -> (rule6 % int3)) triple4) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple5 triple3) -> (rule6 % int5)) ((((triple5 triple3) -> (rule6 % int5)) ((triple3) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
((((((triple5 triple3) -> (rule6 % int5)) ((((triple5 triple3) -> (rule6 % int5)) ((triple5) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
((((triple1) -> (rule7 % int4)) ((((((triple1) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Erin is big.
("Erin" "is" "big" "+")
((triple2 ((triple2 ((((triple2) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule7 % int5)) ((((triple1) -> (rule7 % int5)) ((((((triple1) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple2 ((triple2 ((((triple2) -> (rule5 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5