Bob is nice. Bob is rough. Bob is not white. Bob is young. Charlie is big. Charlie is furry. Charlie is nice. Charlie is smart. Charlie is white. Charlie is not young. If something is big then it is not rough.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
If something is big then it is not rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
Charlie is furry.
True
1
proof
[(triple6)]
("Charlie" "is" "furry" "+")
triple6
Charlie is not white.
False
1
inv-proof
[(triple9)]
("Charlie" "is" "white" "-")
triple9
Charlie is not rough.
True
2
proof
[(((triple5) -> rule1))]
("Charlie" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is rough.
False
2
inv-proof
[(((triple5) -> rule1))]
("Charlie" "is" "rough" "+")
((triple5) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is nice.[(triple1)] Bob is not white.[(triple3)] Bob is rough.[(triple2)] Bob is young.[(triple4)] Charlie is big.[(triple5)] Charlie is furry.[(triple6)] Charlie is nice.[(triple7)] Charlie is not young.[(triple10)] Charlie is smart.[(triple8)] Charlie is white.[(triple9)] @1: Charlie is not rough.[(((triple5) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is not young.
("Charlie" "is" "young" "-")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Charlie is not rough.
("Charlie" "is" "rough" "-")
((triple5) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1