Bob is rough. Dave is blue. Gary is smart. If Bob is blue and Bob is young then Bob is rough. If something is white and smart then it is rough. Nice things are red. All young, blue things are rough. If something is rough and young then it is blue. All white things are young. All young things are smart. Blue things are nice.
Bob is rough.
("Bob" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Bob is blue and Bob is young then Bob is rough.
((("Bob" "is" "blue" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "rough" "+"))
If something is white and smart then it is rough.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
All young, blue things are rough.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough and young then it is blue.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is nice.
True
2
proof
[(((triple2) -> rule8))]
("Dave" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("Dave" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
True
3
proof
[(((((triple2) -> rule8)) -> rule3))]
("Dave" "is" "red" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule3))]
("Dave" "is" "red" "-")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "young" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is rough.[(triple1)] Dave is blue.[(triple2)] Gary is smart.[(triple3)] @1: Dave is nice.[(((triple2) -> rule8))] @2: Dave is red.[(((((triple2) -> rule8)) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2