Charlie is cold. Charlie is not nice. Charlie is red. Dave is cold. Dave is furry. Dave is green. Dave is kind. Dave is nice. Dave is smart. Erin is cold. Erin is furry. Erin is green. Erin is not kind. Erin is nice. Erin is red. If something is kind and furry then it is nice. If something is red and furry then it is nice. If Dave is kind and Dave is nice then Dave is cold. Nice things are red. If something is smart then it is red. If Dave is furry then Dave is kind. If Erin is cold and Erin is not furry then Erin is not kind. If Dave is nice and Dave is not cold then Dave is green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
If something is kind and furry then it is nice.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is red and furry then it is nice.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Dave is kind and Dave is nice then Dave is cold.
((("Dave" "is" "kind" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "cold" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If Dave is furry then Dave is kind.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "kind" "+"))
If Erin is cold and Erin is not furry then Erin is not kind.
((("Erin" "is" "cold" "+") ("Erin" "is" "furry" "~")) -> ("Erin" "is" "kind" "-"))
If Dave is nice and Dave is not cold then Dave is green.
((("Dave" "is" "nice" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple15 OR ((triple14) -> rule4))]
("Erin" "is" "red" "+")
triple15
((triple14) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Dave is not nice.
False
1
inv-proof
[(triple8 OR ((triple7 triple5) -> rule1) OR ((((triple5) -> rule6) triple5) -> rule1) OR ((((triple9) -> rule5) triple5) -> rule2))]
("Dave" "is" "nice" "-")
triple8
((triple7 triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
True
2
proof
[(((triple8) -> rule4) OR ((triple9) -> rule5) OR ((((triple7 triple5) -> rule1)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule1)) -> rule4))]
("Dave" "is" "red" "+")
((triple8) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple9) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple5) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not red.
False
2
inv-proof
[(((triple8) -> rule4) OR ((triple9) -> rule5) OR ((((triple7 triple5) -> rule1)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule1)) -> rule4))]
("Dave" "is" "red" "-")
((triple8) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple9) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple5) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is cold.[(triple1)] Charlie is not nice.[(triple2)] Charlie is red.[(triple3)] Dave is cold.[(triple4 OR ((triple7 triple8) -> rule3) OR ((triple7 ((triple7 triple5) -> rule1)) -> rule3) OR ((((triple5) -> rule6) triple8) -> rule3) OR ((((triple5) -> rule6) ((triple7 triple5) -> rule1)) -> rule3) OR ((triple7 ((((triple5) -> rule6) triple5) -> rule1)) -> rule3) OR ((triple7 ((((triple9) -> rule5) triple5) -> rule2)) -> rule3) OR ((((triple5) -> rule6) ((((triple5) -> rule6) triple5) -> rule1)) -> rule3) OR ((((triple5) -> rule6) ((((triple9) -> rule5) triple5) -> rule2)) -> rule3))] Dave is furry.[(triple5)] Dave is green.[(triple6)] Dave is kind.[(triple7 OR ((triple5) -> rule6))] Dave is nice.[(triple8 OR ((triple7 triple5) -> rule1) OR ((((triple5) -> rule6) triple5) -> rule1) OR ((((triple9) -> rule5) triple5) -> rule2))] Dave is smart.[(triple9)] Erin is cold.[(triple10)] Erin is furry.[(triple11)] Erin is green.[(triple12)] Erin is nice.[(triple14 OR ((triple15 triple11) -> rule2))] Erin is not kind.[(triple13)] Erin is red.[(triple15 OR ((triple14) -> rule4))] @1: Dave is red.[(((triple8) -> rule4) OR ((triple9) -> rule5) OR ((((triple7 triple5) -> rule1)) -> rule4) OR ((((((triple5) -> rule6) triple5) -> rule1)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple7 triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple7 ((triple7 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple5) -> (rule6 % int2)) triple8) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple7 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple7 ((((triple5) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple7 ((((triple9) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((((triple5) -> (rule6 % int3)) ((((triple5) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((((triple5) -> (rule6 % int4)) ((((triple9) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
((triple5) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple7 triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple9) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Erin is cold.
("Erin" "is" "cold" "+")
triple10
Erin is furry.
("Erin" "is" "furry" "+")
triple11
Erin is green.
("Erin" "is" "green" "+")
triple12
Erin is nice.
("Erin" "is" "nice" "+")
triple14
((triple15 triple11) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not kind.
("Erin" "is" "kind" "-")
triple13
Erin is red.
("Erin" "is" "red" "+")
triple15
((triple14) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple8) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple9) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple7 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple5) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3