Dave is red. Gary is cold. All red things are big. If something is kind then it is not nice. If something is red then it is not nice. If Dave is not rough then Dave is kind. If Dave is rough then Dave is kind. If something is big and kind then it is cold. If something is kind and red then it is not blue. If something is big then it is kind.
Dave is red.
("Dave" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is not nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "-"))
If something is red then it is not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If Dave is not rough then Dave is kind.
((("Dave" "is" "rough" "~")) -> ("Dave" "is" "kind" "+"))
If Dave is rough then Dave is kind.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "kind" "+"))
If something is big and kind then it is cold.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is kind and red then it is not blue.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Dave is big.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "big" "+")
((triple1) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule8)) -> rule2))]
("Dave" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not blue.
True
5
proof
[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule7))]
("Dave" "is" "blue" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule7))]
("Dave" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Dave is red.[(triple1)] Gary is cold.[(triple2)] @1: Dave is big.[(((triple1) -> rule1))] Dave is not nice.[(((triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule8)) -> rule2))] @2: Dave is kind.[(((((triple1) -> rule1)) -> rule8))] @3: Dave is cold.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule8)) -> rule6))] Dave is not blue.[(((((((triple1) -> rule1)) -> rule8) triple1) -> rule7))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not nice.
("Dave" "is" "nice" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3