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