Anne is smart. Gary is round. Harry is quiet. All round, smart things are kind. If Anne is round then Anne is quiet. If something is white then it is quiet. If something is round and smart then it is big. All round, quiet things are kind. All smart, big things are rough. If something is white then it is big. If something is smart then it is round.
Anne is smart.
("Anne" "is" "smart" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All round, smart things are kind.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If Anne is round then Anne is quiet.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "quiet" "+"))
If something is white then it is quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is round and smart then it is big.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All round, quiet things are kind.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All smart, big things are rough.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is smart then it is round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Gary is round.
True
1
proof
[(triple2)]
("Gary" "is" "round" "+")
triple2
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "round" "+")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "round" "-")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is smart.[(triple1)] Gary is round.[(triple2)] Harry is quiet.[(triple3)] @1: Anne is round.[(((triple1) -> rule8))] @2: Anne is big.[(((((triple1) -> rule8) triple1) -> rule4))] Anne is kind.[(((((triple1) -> rule8) triple1) -> rule1) OR ((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule2)) -> rule5))] Anne is quiet.[(((((triple1) -> rule8)) -> rule2))] @3: Anne is rough.[(((triple1 ((((triple1) -> rule8) triple1) -> rule4)) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Gary is round.
("Gary" "is" "round" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3