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