Dave is not young. Erin is big. Erin is blue. Erin is not furry. Erin is white. Fiona is not blue. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is white. Harry is young. If Dave is not green then Dave is kind. If something is furry then it is blue. All kind things are blue. If something is white and green then it is not big. All blue things are white. Kind things are furry.
Dave is not young.
("Dave" "is" "young" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is white.
("Erin" "is" "white" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is not green then Dave is kind.
((("Dave" "is" "green" "~")) -> ("Dave" "is" "kind" "+"))
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is white and green then it is not big.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Harry is green.
True
1
proof
[(triple9)]
("Harry" "is" "green" "+")
triple9
Dave is young.
False
1
inv-proof
[(triple1)]
("Dave" "is" "young" "+")
triple1
Harry is not big.
True
3
proof
[(((triple11 triple9) -> rule4) OR ((((triple7) -> rule5) triple9) -> rule4) OR ((((((triple10) -> rule3)) -> rule5) triple9) -> rule4) OR ((((((triple8) -> rule2)) -> rule5) triple9) -> rule4) OR ((((((((triple10) -> rule6)) -> rule2)) -> rule5) triple9) -> rule4))]
("Harry" "is" "big" "-")
((triple11 triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
((((triple7) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is big.
False
3
inv-proof
[(((triple11 triple9) -> rule4) OR ((((triple7) -> rule5) triple9) -> rule4) OR ((((((triple10) -> rule3)) -> rule5) triple9) -> rule4) OR ((((((triple8) -> rule2)) -> rule5) triple9) -> rule4) OR ((((((((triple10) -> rule6)) -> rule2)) -> rule5) triple9) -> rule4))]
("Harry" "is" "big" "+")
((triple11 triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
((((triple7) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Dave is not blue.
Unknown
inv-rconc
[@3: Dave is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Dave is not young.[(triple1)] Erin is big.[(triple2)] Erin is blue.[(triple3)] Erin is not furry.[(triple4)] Erin is white.[(triple5 OR ((triple3) -> rule5))] Fiona is not blue.[(triple6)] Harry is blue.[(triple7 OR ((triple10) -> rule3) OR ((triple8) -> rule2) OR ((((triple10) -> rule6)) -> rule2))] Harry is furry.[(triple8 OR ((triple10) -> rule6))] Harry is green.[(triple9)] Harry is kind.[(triple10)] Harry is white.[(triple11 OR ((triple7) -> rule5) OR ((((triple10) -> rule3)) -> rule5) OR ((((triple8) -> rule2)) -> rule5) OR ((((((triple10) -> rule6)) -> rule2)) -> rule5))] Harry is young.[(triple12)] @1: Harry is not big.[(((triple11 triple9) -> rule4) OR ((((triple7) -> rule5) triple9) -> rule4) OR ((((((triple10) -> rule3)) -> rule5) triple9) -> rule4) OR ((((((triple8) -> rule2)) -> rule5) triple9) -> rule4) OR ((((((((triple10) -> rule6)) -> rule2)) -> rule5) triple9) -> rule4))]
Dave is not young.
("Dave" "is" "young" "-")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is not furry.
("Erin" "is" "furry" "-")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
((triple3) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple10) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple8) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((triple10) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple7) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple10) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is not big.
("Harry" "is" "big" "-")
((triple11 triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
((((triple7) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple10) -> (rule3 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple8) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((((triple10) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4