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