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