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