Anne is kind. Anne is young. Dave is kind. Dave is young. Erin is cold. Erin is kind. Erin is quiet. Erin is red. Erin is smart. Erin is young. Gary is cold. Gary is kind. Gary is nice. Gary is red. Gary is smart. All young people are smart. All kind, smart people are red. If someone is red then they are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All kind, smart people are red.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Erin is cold.
True
1
proof
[(triple5)]
("Erin" "is" "cold" "+")
triple5
Gary is not red.
False
1
inv-proof
[(triple14 OR ((triple12 triple15) -> rule2))]
("Gary" "is" "red" "-")
triple14
((triple12 triple15) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Erin is nice.
True
2
proof
[(((triple8) -> rule3) OR ((((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 ((triple10) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "nice" "+")
((triple8) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 ((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not nice.
False
2
inv-proof
[(((triple8) -> rule3) OR ((((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 ((triple10) -> rule1)) -> rule2)) -> rule3))]
("Erin" "is" "nice" "-")
((triple8) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 ((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Anne is red.
True
4
proof
[(((triple1 ((triple2) -> rule1)) -> rule2))]
("Anne" "is" "red" "+")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
False
4
inv-proof
[(((triple1 ((triple2) -> rule1)) -> rule2))]
("Anne" "is" "red" "-")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
True
5
proof
[(((((triple1 ((triple2) -> rule1)) -> rule2)) -> rule3))]
("Anne" "is" "nice" "+")
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((((triple3 ((triple4) -> rule1)) -> rule2)) -> rule3))]
("Dave" "is" "nice" "-")
((((triple3 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is kind.[(triple1)] Anne is young.[(triple2)] Dave is kind.[(triple3)] Dave is young.[(triple4)] Erin is cold.[(triple5)] Erin is kind.[(triple6)] Erin is quiet.[(triple7)] Erin is red.[(triple8 OR ((triple6 triple9) -> rule2) OR ((triple6 ((triple10) -> rule1)) -> rule2))] Erin is smart.[(triple9 OR ((triple10) -> rule1))] Erin is young.[(triple10)] Gary is cold.[(triple11)] Gary is kind.[(triple12)] Gary is nice.[(triple13 OR ((triple14) -> rule3) OR ((((triple12 triple15) -> rule2)) -> rule3))] Gary is red.[(triple14 OR ((triple12 triple15) -> rule2))] Gary is smart.[(triple15)] @1: Anne is smart.[(((triple2) -> rule1))] Dave is smart.[(((triple4) -> rule1))] Erin is nice.[(((triple8) -> rule3) OR ((((triple6 triple9) -> rule2)) -> rule3) OR ((((triple6 ((triple10) -> rule1)) -> rule2)) -> rule3))] @2: Anne is red.[(((triple1 ((triple2) -> rule1)) -> rule2))] Dave is red.[(((triple3 ((triple4) -> rule1)) -> rule2))] @3: Anne is nice.[(((((triple1 ((triple2) -> rule1)) -> rule2)) -> rule3))] Dave is nice.[(((((triple3 ((triple4) -> rule1)) -> rule2)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple6 triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple6 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple10) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
((triple14) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple12 triple15) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple14
((triple12 triple15) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple15
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple8) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple6 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple6 ((triple10) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple3 ((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1 ((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple3 ((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3