Dave is green. Dave is red. Dave is rough. Erin is nice. Erin is red. Erin is round. Gary is green. Gary is nice. Gary is round. Gary is smart. Nice things are green. If Erin is red and Erin is rough then Erin is smart. If something is round and green then it is rough.
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If Erin is red and Erin is rough then Erin is smart.
((("Erin" "is" "red" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
If something is round and green then it is rough.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Gary is green.
True
1
proof
[(triple7 OR ((triple8) -> rule1))]
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not round.
False
1
inv-proof
[(triple9)]
("Gary" "is" "round" "-")
triple9
Gary is rough.
True
3
proof
[(((triple9 triple7) -> rule3) OR ((triple9 ((triple8) -> rule1)) -> rule3))]
("Gary" "is" "rough" "+")
((triple9 triple7) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple9 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not rough.
False
3
inv-proof
[(((triple9 triple7) -> rule3) OR ((triple9 ((triple8) -> rule1)) -> rule3))]
("Gary" "is" "rough" "-")
((triple9 triple7) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple9 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Erin is rough.
True
4
proof
[(((triple6 ((triple4) -> rule1)) -> rule3))]
("Erin" "is" "rough" "+")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not rough.
False
4
inv-proof
[(((triple6 ((triple4) -> rule1)) -> rule3))]
("Erin" "is" "rough" "-")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
True
6
proof
[(((triple5 ((triple6 ((triple4) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "smart" "+")
((triple5 ((triple6 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((triple5 ((triple6 ((triple4) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "smart" "-")
((triple5 ((triple6 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is green.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Erin is nice.[(triple4)] Erin is red.[(triple5)] Erin is round.[(triple6)] Gary is green.[(triple7 OR ((triple8) -> rule1))] Gary is nice.[(triple8)] Gary is round.[(triple9)] Gary is smart.[(triple10)] @1: Erin is green.[(((triple4) -> rule1))] Gary is rough.[(((triple9 triple7) -> rule3) OR ((triple9 ((triple8) -> rule1)) -> rule3))] @2: Erin is rough.[(((triple6 ((triple4) -> rule1)) -> rule3))] @3: Erin is smart.[(((triple5 ((triple6 ((triple4) -> rule1)) -> rule3)) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple8) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple9 triple7) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple9 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 ((triple6 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3