Bob is blue. Bob is cold. Bob is green. Bob is red. Bob is rough. Bob is smart. Dave is blue. Dave is cold. Dave is green. Dave is rough. Dave is round. Gary is not blue. Gary is cold. Gary is green. Gary is rough. Gary is round. If Gary is blue and Gary is not green then Gary is cold. If someone is blue then they are red. All green, red people are smart. All cold people are rough. If Bob is round and Bob is not smart then Bob is rough. If someone is rough and red then they are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If Gary is blue and Gary is not green then Gary is cold.
((("Gary" "is" "blue" "+") ("Gary" "is" "green" "~")) -> ("Gary" "is" "cold" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
All green, red people are smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If Bob is round and Bob is not smart then Bob is rough.
((("Bob" "is" "round" "+") ("Bob" "is" "smart" "~")) -> ("Bob" "is" "rough" "+"))
If someone is rough and red then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Dave is blue.
True
1
proof
[(triple7)]
("Dave" "is" "blue" "+")
triple7
Dave is not cold.
False
1
inv-proof
[(triple8)]
("Dave" "is" "cold" "-")
triple8
Dave is red.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "red" "+")
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "red" "-")
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
True
4
proof
[(((triple9 ((triple7) -> rule2)) -> rule3))]
("Dave" "is" "smart" "+")
((triple9 ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not smart.
False
4
inv-proof
[(((triple9 ((triple7) -> rule2)) -> rule3))]
("Dave" "is" "smart" "-")
((triple9 ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Gary" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3)] Bob is red.[(triple4 OR ((triple1) -> rule2))] Bob is rough.[(triple5 OR ((triple2) -> rule4))] Bob is smart.[(triple6 OR ((triple3 triple4) -> rule3) OR ((triple3 ((triple1) -> rule2)) -> rule3))] Dave is blue.[(triple7)] Dave is cold.[(triple8)] Dave is green.[(triple9)] Dave is rough.[(triple10 OR ((triple8) -> rule4))] Dave is round.[(triple11 OR ((triple10 ((triple7) -> rule2)) -> rule6) OR ((((triple8) -> rule4) ((triple7) -> rule2)) -> rule6))] Gary is cold.[(triple13)] Gary is green.[(triple14)] Gary is not blue.[(triple12)] Gary is rough.[(triple15 OR ((triple13) -> rule4))] Gary is round.[(triple16)] @1: Bob is round.[(((triple5 triple4) -> rule6) OR ((triple5 ((triple1) -> rule2)) -> rule6) OR ((((triple2) -> rule4) triple4) -> rule6) OR ((((triple2) -> rule4) ((triple1) -> rule2)) -> rule6))] Dave is red.[(((triple7) -> rule2))] @2: Dave is smart.[(((triple9 ((triple7) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple1) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3 triple4) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple10
((triple8) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple11
((triple10 ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is not blue.
("Gary" "is" "blue" "-")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((triple13) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple16
Bob is round.
("Bob" "is" "round" "+")
((triple5 triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple2) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((triple7) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple9 ((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2