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