Anne is blue. Anne is green. Anne is smart. Bob is green. Bob is kind. Bob is smart. Dave is kind. Dave is not nice. Harry is not kind. Harry is young. If something is big then it is blue. Big things are not young. Blue, nice things are big. If something is blue then it is big. If something is nice and not green then it is not kind. If something is blue and not young then it is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is young.
("Harry" "is" "young" "+")
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
Blue, nice things are big.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is nice and not green then it is not kind.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "kind" "-"))
If something is blue and not young then it is kind.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "kind" "+"))
Anne is smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Bob is not green.
False
1
inv-proof
[(triple4)]
("Bob" "is" "green" "-")
triple4
Anne is big.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "big" "-")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not young.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "kind" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not kind.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "kind" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is big.
Unknown
rconc
[@3: Dave is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Dave" "is" "big" "+")
Harry is not big.
Unknown
inv-rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("Harry" "is" "big" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "blue" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is smart.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is smart.[(triple6)] Dave is kind.[(triple7)] Dave is not nice.[(triple8)] Harry is not kind.[(triple9)] Harry is young.[(triple10)] @1: Anne is big.[(((triple1) -> rule4))] @2: Anne is not young.[(((((triple1) -> rule4)) -> rule2))] @3: Anne is kind.[(((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is not nice.
("Dave" "is" "nice" "-")
triple8
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
int2
Anne is big.
("Anne" "is" "big" "+")
int3