Bob is blue. Dave is big. If Bob is red and Bob is round then Bob is big. Blue things are rough. Rough things are nice. If something is big and rough then it is red. Round things are rough. Round things are rough. If something is big then it is nice. All rough, red things are round.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
If Bob is red and Bob is round then Bob is big.
((("Bob" "is" "red" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "big" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is big and rough then it is red.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
All rough, red things are round.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is red.
Unknown
rconc
[@3: Dave is red.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule8 <- FAIL)]]
("Dave" "is" "red" "+")
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Dave is big.[(triple2)] @1: Bob is rough.[(((triple1) -> rule2))] Dave is nice.[(((triple2) -> rule7))] @2: Bob is nice.[(((((triple1) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2