Bob is cold. Bob is red. Dave is kind. Red things are big. All cold things are not smart. If something is big and not cold then it is not smart. If something is big and smart then it is white. Kind things are not white. If Dave is cold and Dave is kind then Dave is big. If Dave is quiet and Dave is white then Dave is not big. If something is kind then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All cold things are not smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "-"))
If something is big and not cold then it is not smart.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "-"))
If something is big and smart then it is white.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Kind things are not white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "-"))
If Dave is cold and Dave is kind then Dave is big.
((("Dave" "is" "cold" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "big" "+"))
If Dave is quiet and Dave is white then Dave is not big.
((("Dave" "is" "quiet" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "big" "-"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Dave is not white.
True
2
proof
[(((triple3) -> rule5))]
("Dave" "is" "white" "-")
((triple3) -> (rule5 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is not red.
False
2
inv-proof
[(((triple3) -> rule8))]
("Dave" "is" "red" "-")
((triple3) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
True
3
proof
[(((((triple3) -> rule8)) -> rule1))]
("Dave" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule1))]
("Dave" "is" "big" "-")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Dave is kind.[(triple3)] @1: Bob is big.[(((triple2) -> rule1))] Bob is not smart.[(((triple1) -> rule2))] Dave is not white.[(((triple3) -> rule5))] Dave is red.[(((triple3) -> rule8))] @2: Dave is big.[(((((triple3) -> rule8)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
((triple3) -> (rule5 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
((triple3) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2