Anne is blue. If someone is cold and young then they are big. If Anne is white and Anne is not cold then Anne is blue. If Anne is blue then Anne is big. All big people are kind. If someone is big and young then they are blue. All cold people are blue. If Anne is blue and Anne is kind then Anne is young. If Anne is not white and Anne is not quiet then Anne is not young.
Anne is blue.
("Anne" "is" "blue" "+")
If someone is cold and young then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If Anne is white and Anne is not cold then Anne is blue.
((("Anne" "is" "white" "+") ("Anne" "is" "cold" "~")) -> ("Anne" "is" "blue" "+"))
If Anne is blue then Anne is big.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and young then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Anne is blue and Anne is kind then Anne is young.
((("Anne" "is" "blue" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
If Anne is not white and Anne is not quiet then Anne is not young.
((("Anne" "is" "white" "~") ("Anne" "is" "quiet" "~")) -> ("Anne" "is" "young" "-"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "-")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "young" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not young.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule7))]
("Anne" "is" "young" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] @1: Anne is big.[(((triple1) -> rule3))] @2: Anne is kind.[(((((triple1) -> rule3)) -> rule4))] @3: Anne is young.[(((triple1 ((((triple1) -> rule3)) -> rule4)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3