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