Anne is nice. Bob is smart. Young, big things are smart. If something is young then it is quiet. If something is green and not young then it is not quiet. All smart things are green. All nice things are not kind. If Anne is young and Anne is nice then Anne is not kind. All green things are nice. If something is green and young then it is nice.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Young, big things are smart.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is green and not young then it is not quiet.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "quiet" "-"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All nice things are not kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
If Anne is young and Anne is nice then Anne is not kind.
((("Anne" "is" "young" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "-"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is green and young then it is nice.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Bob is smart.
True
1
proof
[(triple2)]
("Bob" "is" "smart" "+")
triple2
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Bob is green.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "green" "+")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Anne is kind.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "kind" "+")
((triple1) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Bob is nice.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("Bob" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not kind.
True
4
proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
("Bob" "is" "kind" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is kind.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
("Bob" "is" "kind" "+")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is nice.[(triple1)] Bob is smart.[(triple2)] @1: Anne is not kind.[(((triple1) -> rule5))] Bob is green.[(((triple2) -> rule4))] @2: Bob is nice.[(((((triple2) -> rule4)) -> rule7))] @3: Bob is not kind.[(((((((triple2) -> rule4)) -> rule7)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule5 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3