Dave is blue. Dave is cold. Dave is kind. Dave is red. Dave is white. Dave is young. Erin is cold. Erin is red. Erin is smart. Erin is white. If someone is young then they are red. Red people are kind. All cold, blue people are kind. If Dave is red and Dave is kind then Dave is young. If Dave is young and Dave is blue then Dave is kind. Smart, white people are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All cold, blue people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Dave is red and Dave is kind then Dave is young.
((("Dave" "is" "red" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "young" "+"))
If Dave is young and Dave is blue then Dave is kind.
((("Dave" "is" "young" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "kind" "+"))
Smart, white people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Erin is cold.
True
1
proof
[(triple7)]
("Erin" "is" "cold" "+")
triple7
Dave is not young.
False
1
inv-proof
[(triple6 OR ((triple4 triple3) -> rule4) OR ((triple4 ((triple4) -> rule2)) -> rule4) OR ((triple4 ((triple2 triple1) -> rule3)) -> rule4))]
("Dave" "is" "young" "-")
triple6
((triple4 triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple4 ((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is kind.
True
2
proof
[(((triple8) -> rule2) OR ((triple7 ((triple9 triple10) -> rule6)) -> rule3))]
("Erin" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple9 triple10) -> (rule6 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
2
inv-proof
[(((triple8) -> rule2) OR ((triple7 ((triple9 triple10) -> rule6)) -> rule3))]
("Erin" "is" "kind" "-")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple9 triple10) -> (rule6 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3 OR ((triple4) -> rule2) OR ((triple2 triple1) -> rule3) OR ((triple6 triple1) -> rule5) OR ((((triple6) -> rule1)) -> rule2))] Dave is red.[(triple4 OR ((triple6) -> rule1))] Dave is white.[(triple5)] Dave is young.[(triple6 OR ((triple4 triple3) -> rule4) OR ((triple4 ((triple4) -> rule2)) -> rule4) OR ((triple4 ((triple2 triple1) -> rule3)) -> rule4))] Erin is cold.[(triple7)] Erin is red.[(triple8)] Erin is smart.[(triple9)] Erin is white.[(triple10)] @1: Erin is blue.[(((triple9 triple10) -> rule6))] Erin is kind.[(((triple8) -> rule2) OR ((triple7 ((triple9 triple10) -> rule6)) -> rule3))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple2 triple1) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple6 triple1) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple6) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple4 triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple4 ((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is smart.
("Erin" "is" "smart" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
((triple9 triple10) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple9 triple10) -> (rule6 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2