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