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