Bob is kind. Bob is young. Charlie is big. Charlie is blue. Charlie is kind. Charlie is quiet. Charlie is smart. Charlie is young. Dave is blue. Dave is quiet. All big people are young.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Charlie is quiet.
True
1
proof
[(triple6)]
("Charlie" "is" "quiet" "+")
triple6
Dave is not blue.
False
1
inv-proof
[(triple9)]
("Dave" "is" "blue" "-")
triple9
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "young" "-")
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 young.[(triple2)] Charlie is big.[(triple3)] Charlie is blue.[(triple4)] Charlie is kind.[(triple5)] Charlie is quiet.[(triple6)] Charlie is smart.[(triple7)] Charlie is young.[(triple8 OR ((triple3) -> rule1))] Dave is blue.[(triple9)] Dave is quiet.[(triple10)]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is young.
("Charlie" "is" "young" "+")
triple8
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is quiet.
("Dave" "is" "quiet" "+")
triple10