Bob is green. Bob is round. Bob is smart. Bob is white. Bob is young. Charlie is blue. Charlie is green. Charlie is quiet. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. Blue things are quiet. If Bob is not blue and Bob is not quiet then Bob is white.
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If Bob is not blue and Bob is not quiet then Bob is white.
((("Bob" "is" "blue" "~") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "white" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple11)]
("Charlie" "is" "white" "-")
triple11
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is green.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3)] Bob is white.[(triple4)] Bob is young.[(triple5)] Charlie is blue.[(triple6)] Charlie is green.[(triple7)] Charlie is quiet.[(triple8 OR ((triple6) -> rule1))] Charlie is round.[(triple9)] Charlie is smart.[(triple10)] Charlie is white.[(triple11)] Charlie is young.[(triple12)]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
((triple6) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Charlie is white.
("Charlie" "is" "white" "+")
triple11
Charlie is young.
("Charlie" "is" "young" "+")
triple12