Charlie is blue. Charlie is red. Charlie is rough. Dave is red. Dave is rough. Dave is round. Dave is not smart. If Charlie is round then Charlie is red. If Dave is not blue and Dave is not white then Dave is rough. If something is cold and not round then it is red. If something is rough and not blue then it is cold. All white things are smart. If Charlie is rough then Charlie is not white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
If Charlie is round then Charlie is red.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
If Dave is not blue and Dave is not white then Dave is rough.
((("Dave" "is" "blue" "~") ("Dave" "is" "white" "~")) -> ("Dave" "is" "rough" "+"))
If something is cold and not round then it is red.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "+"))
If something is rough and not blue then it is cold.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
All white things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Charlie is rough then Charlie is not white.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "white" "-"))
Dave is rough.
True
1
proof
[(triple5)]
("Dave" "is" "rough" "+")
triple5
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
Charlie is not white.
True
2
proof
[(((triple3) -> rule6))]
("Charlie" "is" "white" "-")
((triple3) -> (rule6 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is white.
False
2
inv-proof
[(((triple3) -> rule6))]
("Charlie" "is" "white" "+")
((triple3) -> (rule6 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Charlie is blue.[(triple1)] Charlie is red.[(triple2)] Charlie is rough.[(triple3)] Dave is not smart.[(triple7)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Dave is round.[(triple6)] @1: Charlie is not white.[(((triple3) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Dave is not smart.
("Dave" "is" "smart" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Charlie is not white.
("Charlie" "is" "white" "-")
((triple3) -> (rule6 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1