Dave is big. Dave is rough. Dave is round. Dave is young. Erin is blue. Erin is quiet. Erin is young. Big, young things are red. If Erin is quiet and Erin is blue then Erin is big. Red things are round.
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Big, young things are red.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If Erin is quiet and Erin is blue then Erin is big.
((("Erin" "is" "quiet" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "big" "+"))
Red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not round.
False
1
inv-proof
[(triple3 OR ((((triple1 triple4) -> rule1)) -> rule3))]
("Dave" "is" "round" "-")
triple3
((((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
True
3
proof
[(((triple1 triple4) -> rule1))]
("Dave" "is" "red" "+")
((triple1 triple4) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
3
inv-proof
[(((triple1 triple4) -> rule1))]
("Dave" "is" "red" "-")
((triple1 triple4) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is red.
True
5
proof
[(((((triple6 triple5) -> rule2) triple7) -> rule1))]
("Erin" "is" "red" "+")
((((triple6 triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not red.
False
5
inv-proof
[(((((triple6 triple5) -> rule2) triple7) -> rule1))]
("Erin" "is" "red" "-")
((((triple6 triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
True
6
proof
[(((((((triple6 triple5) -> rule2) triple7) -> rule1)) -> rule3))]
("Erin" "is" "round" "+")
((((((triple6 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not round.
False
6
inv-proof
[(((((((triple6 triple5) -> rule2) triple7) -> rule1)) -> rule3))]
("Erin" "is" "round" "-")
((((((triple6 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is big.[(triple1)] Dave is rough.[(triple2)] Dave is round.[(triple3 OR ((((triple1 triple4) -> rule1)) -> rule3))] Dave is young.[(triple4)] Erin is blue.[(triple5)] Erin is quiet.[(triple6)] Erin is young.[(triple7)] @1: Dave is red.[(((triple1 triple4) -> rule1))] Erin is big.[(((triple6 triple5) -> rule2))] @2: Erin is red.[(((((triple6 triple5) -> rule2) triple7) -> rule1))] @3: Erin is round.[(((((((triple6 triple5) -> rule2) triple7) -> rule1)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
((((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
((triple1 triple4) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple6 triple5) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple6 triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple6 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3