Bob is furry. Gary is red. Blue people are big. White, red people are blue. If someone is furry then they are quiet. If Bob is blue then Bob is red. Red, furry people are big. Furry people are nice. All red people are big. If someone is quiet then they are blue.
Bob is furry.
("Bob" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
White, red people are blue.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is blue then Bob is red.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "red" "+"))
Red, furry people are big.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple2)]
("Gary" "is" "red" "-")
triple2
Gary is big.
True
2
proof
[(((triple2) -> rule7))]
("Gary" "is" "big" "+")
((triple2) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "nice" "-")
((triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is red.
True
4
proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule4))]
("Bob" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule4)) -> rule7) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule4) triple1) -> rule5))]
("Bob" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is furry.[(triple1)] Gary is red.[(triple2)] @1: Bob is nice.[(((triple1) -> rule6))] Bob is quiet.[(((triple1) -> rule3))] Gary is big.[(((triple2) -> rule7))] @2: Bob is blue.[(((((triple1) -> rule3)) -> rule8))] @3: Bob is big.[(((((((triple1) -> rule3)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule4)) -> rule7) OR ((((((((triple1) -> rule3)) -> rule8)) -> rule4) triple1) -> rule5))] Bob is red.[(((((((triple1) -> rule3)) -> rule8)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple2) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3