Anne is big. Anne is cold. Anne is kind. Dave is kind. Dave is red. Dave is young. Gary is big. Gary is cold. Gary is kind. Gary is smart. If Anne is cold and Anne is big then Anne is red. If someone is furry then they are kind. Furry, cold people are smart. If Anne is kind then Anne is young. Kind, young people are big. Young, kind people are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Anne is cold and Anne is big then Anne is red.
((("Anne" "is" "cold" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "red" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Furry, cold people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
If Anne is kind then Anne is young.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
Kind, young people are big.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Young, kind people are smart.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Anne is big.
True
1
proof
[(triple1 OR ((triple3 ((triple3) -> rule4)) -> rule5))]
("Anne" "is" "big" "+")
triple1
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Dave is smart.
True
3
proof
[(((triple6 triple4) -> rule6))]
("Dave" "is" "smart" "+")
((triple6 triple4) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is not red.
False
3
inv-proof
[(((triple2 triple1) -> rule1) OR ((triple2 ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule1))]
("Anne" "is" "red" "-")
((triple2 triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is big.[(triple1 OR ((triple3 ((triple3) -> rule4)) -> rule5))] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5)] Dave is young.[(triple6)] Gary is big.[(triple7)] Gary is cold.[(triple8)] Gary is kind.[(triple9)] Gary is smart.[(triple10)] @1: Anne is red.[(((triple2 triple1) -> rule1) OR ((triple2 ((triple3 ((triple3) -> rule4)) -> rule5)) -> rule1))] Anne is young.[(((triple3) -> rule4))] Dave is big.[(((triple4 triple6) -> rule5))] Dave is smart.[(((triple6 triple4) -> rule6))] @2: Anne is smart.[(((((triple3) -> rule4) triple3) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 ((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple4 triple6) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple6 triple4) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2