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