Bob is green. Bob is nice. Bob is quiet. Bob is red. Bob is round. Charlie is big. Charlie is quiet. Round people are rough. Nice people are red. If someone is green then they are red. If someone is nice and rough then they are red. If someone is green and rough then they are nice. If Bob is rough and Bob is red then Bob is round.
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and rough then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is green and rough then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Bob is rough and Bob is red then Bob is round.
((("Bob" "is" "rough" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "round" "+"))
Bob is red.
True
1
proof
[(triple4 OR ((triple1) -> rule3) OR ((triple2) -> rule2) OR ((triple2 ((triple5) -> rule1)) -> rule4) OR ((((triple1 ((triple5) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple5) -> rule1)) -> rule5) ((triple5) -> rule1)) -> rule4))]
("Bob" "is" "red" "+")
triple4
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2 ((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2)) ((triple5) -> (rule1 % int3))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not red.
False
1
inv-proof
[(triple4 OR ((triple1) -> rule3) OR ((triple2) -> rule2) OR ((triple2 ((triple5) -> rule1)) -> rule4) OR ((((triple1 ((triple5) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple5) -> rule1)) -> rule5) ((triple5) -> rule1)) -> rule4))]
("Bob" "is" "red" "-")
triple4
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2 ((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2)) ((triple5) -> (rule1 % int3))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is green.[(triple1)] Bob is nice.[(triple2 OR ((triple1 ((triple5) -> rule1)) -> rule5))] Bob is quiet.[(triple3)] Bob is red.[(triple4 OR ((triple1) -> rule3) OR ((triple2) -> rule2) OR ((triple2 ((triple5) -> rule1)) -> rule4) OR ((((triple1 ((triple5) -> rule1)) -> rule5)) -> rule2) OR ((((triple1 ((triple5) -> rule1)) -> rule5) ((triple5) -> rule1)) -> rule4))] Bob is round.[(triple5)] Charlie is big.[(triple6)] Charlie is quiet.[(triple7)] @1: Bob is rough.[(((triple5) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple1 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple1) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple2 ((triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((triple1 ((triple5) -> (rule1 % int3))) -> (rule5 % int2)) ((triple5) -> (rule1 % int3))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1