Anne is quiet. Anne is rough. Anne is young. Dave is nice. Dave is quiet. Dave is round. Dave is smart. Young, red things are nice. All red things are round. Quiet things are smart. Nice, young things are quiet. Quiet, young things are smart. If something is smart then it is red. All smart things are quiet. If something is rough and nice then it is smart.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Young, red things are nice.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Nice, young things are quiet.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Quiet, young things are smart.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is rough and nice then it is smart.
((("something" "is" "rough" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is smart.
True
2
proof
[(((triple1) -> rule3) OR ((triple1 triple3) -> rule5))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple7) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("Dave" "is" "red" "-")
((triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Anne is red.
True
3
proof
[(((((triple1) -> rule3)) -> rule6) OR ((((triple1 triple3) -> rule5)) -> rule6))]
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple1 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6) OR ((((triple1 triple3) -> rule5)) -> rule6))]
("Anne" "is" "red" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple1 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2) OR ((((((triple1 triple3) -> rule5)) -> rule6)) -> rule2))]
("Anne" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple1 triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not nice.
False
5
inv-proof
[(((triple3 ((((triple1) -> rule3)) -> rule6)) -> rule1) OR ((triple3 ((((triple1 triple3) -> rule5)) -> rule6)) -> rule1))]
("Anne" "is" "nice" "-")
((triple3 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple3 ((((triple1 triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % 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 rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is quiet.[(triple1)] Anne is rough.[(triple2)] Anne is young.[(triple3)] Dave is nice.[(triple4)] Dave is quiet.[(triple5 OR ((triple7) -> rule7))] Dave is round.[(triple6 OR ((((triple7) -> rule6)) -> rule2) OR ((((((triple5) -> rule3)) -> rule6)) -> rule2))] Dave is smart.[(triple7 OR ((triple5) -> rule3))] @1: Anne is smart.[(((triple1) -> rule3) OR ((triple1 triple3) -> rule5))] Dave is red.[(((triple7) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] @2: Anne is red.[(((((triple1) -> rule3)) -> rule6) OR ((((triple1 triple3) -> rule5)) -> rule6))] @3: Anne is nice.[(((triple3 ((((triple1) -> rule3)) -> rule6)) -> rule1) OR ((triple3 ((((triple1 triple3) -> rule5)) -> rule6)) -> rule1))] Anne is round.[(((((((triple1) -> rule3)) -> rule6)) -> rule2) OR ((((((triple1 triple3) -> rule5)) -> rule6)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((triple7) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple6
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
triple7
((triple5) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple7) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple1 triple3) -> (rule5 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((triple3 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple3 ((((triple1 triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple1 triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3