Bob is kind. Bob is nice. Bob is rough. Charlie is blue. Charlie is not quiet. Charlie is round. Charlie is young. If something is round then it is young. All kind, rough things are round. Round, quiet things are rough.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
All kind, rough things are round.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Round, quiet things are rough.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Charlie is blue.
True
1
proof
[(triple4)]
("Charlie" "is" "blue" "+")
triple4
Charlie is not blue.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "blue" "-")
triple4
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is rough.[(triple3)] Charlie is blue.[(triple4)] Charlie is not quiet.[(triple5)] Charlie is round.[(triple6)] Charlie is young.[(triple7 OR ((triple6) -> rule1))] @1: Bob is round.[(((triple1 triple3) -> rule2))] @2: Bob is young.[(((((triple1 triple3) -> rule2)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple6) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1 triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2