Bob is green. Dave is big. Gary is smart. Big things are white. If something is big and nice then it is green. All white, round things are big. All red, nice things are round. If something is round then it is nice. If something is white then it is red. Nice things are round. If Dave is red and Dave is big then Dave is round.
Bob is green.
("Bob" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is big and nice then it is green.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All white, round things are big.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All red, nice things are round.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If Dave is red and Dave is big then Dave is round.
((("Dave" "is" "red" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "round" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Gary is not smart.
False
1
inv-proof
[(triple3)]
("Gary" "is" "smart" "-")
triple3
Dave is white.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "white" "+")
((triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "white" "-")
((triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("Dave" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not red.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("Dave" "is" "red" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
True
5
proof
[(((((((triple2) -> rule1)) -> rule6) triple2) -> rule8))]
("Dave" "is" "round" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not round.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule6) triple2) -> rule8))]
("Dave" "is" "round" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule7 <- FAIL)]]
("Bob" "is" "round" "+")
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is round.
Unknown
rconc
[@3: Gary is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule7 <- FAIL)]]
("Gary" "is" "round" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is green.[(triple1)] Dave is big.[(triple2)] Gary is smart.[(triple3)] @1: Dave is white.[(((triple2) -> rule1))] @2: Dave is red.[(((((triple2) -> rule1)) -> rule6))] @3: Dave is round.[(((((((triple2) -> rule1)) -> rule6) triple2) -> rule8))] @4: Dave is nice.[(((((((((triple2) -> rule1)) -> rule6) triple2) -> rule8)) -> rule5))] @5: Dave is green.[(((triple2 ((((((((triple2) -> rule1)) -> rule6) triple2) -> rule8)) -> rule5)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2)) triple2) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule6 % int3)) triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is green.
("Dave" "is" "green" "+")
((triple2 ((((((((triple2) -> (rule1 % int5))) -> (rule6 % int4)) triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
int5