The dog is big. If the dog is blue and the dog is nice then the dog is rough. Big things are red. If the dog is red then the dog is blue.
The dog is big.
("dog" "is" "big" "+")
If the dog is blue and the dog is nice then the dog is rough.
((("dog" "is" "blue" "+") ("dog" "is" "nice" "+")) -> ("dog" "is" "rough" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If the dog is red then the dog is blue.
((("dog" "is" "red" "+")) -> ("dog" "is" "blue" "+"))
The dog is big.
True
1
proof
[(triple1)]
("dog" "is" "big" "+")
triple1
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The dog is red.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "red" "+")
((triple1) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "red" "-")
((triple1) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("dog" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("dog" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "rough" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog is big.[(triple1)] @1: The dog is red.[(((triple1) -> rule2))] @2: The dog is blue.[(((((triple1) -> rule2)) -> rule3))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
((triple1) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2