Bob is nice. Bob is not quiet. Bob is red. Bob is rough. Bob is not white. Dave is big. Dave is quiet. Dave is not white. Gary is not big. Gary is green. Gary is quiet. Gary is not white. If Dave is nice then Dave is red. All quiet things are green. If something is white and green then it is quiet. If something is quiet then it is nice. If something is red and not green then it is rough. If something is red then it is rough.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not white.
("Dave" "is" "white" "-")
Gary is not big.
("Gary" "is" "big" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not white.
("Gary" "is" "white" "-")
If Dave is nice then Dave is red.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "red" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is white and green then it is quiet.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is red and not green then it is rough.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Dave is not white.
True
1
proof
[(triple8)]
("Dave" "is" "white" "-")
triple8
Gary is big.
False
1
inv-proof
[(triple9)]
("Gary" "is" "big" "+")
triple9
Gary is nice.
True
2
proof
[(((triple11) -> rule4))]
("Gary" "is" "nice" "+")
((triple11) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple7) -> rule4))]
("Dave" "is" "nice" "-")
((triple7) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
True
3
proof
[(((((triple7) -> rule4)) -> rule1))]
("Dave" "is" "red" "+")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule1))]
("Dave" "is" "red" "-")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
True
4
proof
[(((((((triple7) -> rule4)) -> rule1)) -> rule6))]
("Dave" "is" "rough" "+")
((((((triple7) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not rough.
False
4
inv-proof
[(((((((triple7) -> rule4)) -> rule1)) -> rule6))]
("Dave" "is" "rough" "-")
((((((triple7) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "rough" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is nice.[(triple1)] Bob is not quiet.[(triple2)] Bob is not white.[(triple5)] Bob is red.[(triple3)] Bob is rough.[(triple4 OR ((triple3) -> rule6))] Dave is big.[(triple6)] Dave is not white.[(triple8)] Dave is quiet.[(triple7)] Gary is green.[(triple10 OR ((triple11) -> rule2))] Gary is not big.[(triple9)] Gary is not white.[(triple12)] Gary is quiet.[(triple11)] @1: Dave is green.[(((triple7) -> rule2))] Dave is nice.[(((triple7) -> rule4))] Gary is nice.[(((triple11) -> rule4))] @2: Dave is red.[(((((triple7) -> rule4)) -> rule1))] @3: Dave is rough.[(((((((triple7) -> rule4)) -> rule1)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is not white.
("Dave" "is" "white" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple11) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not big.
("Gary" "is" "big" "-")
triple9
Gary is not white.
("Gary" "is" "white" "-")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
((triple7) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple11) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple7) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3