Bob is green. Dave is blue. Dave is kind. If Dave is furry and Dave is white then Dave is blue. All smart people are kind. If someone is big and not blue then they are green. If Bob is smart and Bob is kind then Bob is big. If someone is green and not blue then they are not smart. All green people are smart.
Bob is green.
("Bob" "is" "green" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If Dave is furry and Dave is white then Dave is blue.
((("Dave" "is" "furry" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "blue" "+"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and not blue then they are green.
((("someone" "is" "big" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "green" "+"))
If Bob is smart and Bob is kind then Bob is big.
((("Bob" "is" "smart" "+") ("Bob" "is" "kind" "+")) -> ("Bob" "is" "big" "+"))
If someone is green and not blue then they are not smart.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "smart" "-"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Bob is green.
True
1
proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Bob is smart.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "kind" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule4))]
("Bob" "is" "big" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not big.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule4))]
("Bob" "is" "big" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is green.[(triple1)] Dave is blue.[(triple2)] Dave is kind.[(triple3)] @1: Bob is smart.[(((triple1) -> rule6))] @2: Bob is kind.[(((((triple1) -> rule6)) -> rule2))] @3: Bob is big.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule4))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3