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