The dog is blue. Blue things are big. Blue, big things are nice. If something is nice and not big then it is green.
The dog is blue.
("dog" "is" "blue" "+")
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Blue, big things are nice.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not big then it is green.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
The dog is blue.
True
1
proof
[(triple1)]
("dog" "is" "blue" "+")
triple1
The dog is not blue.
False
1
inv-proof
[(triple1)]
("dog" "is" "blue" "-")
triple1
The dog is big.
True
2
proof
[(((triple1) -> rule1))]
("dog" "is" "big" "+")
((triple1) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "is" "big" "-")
((triple1) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("dog" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("dog" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "green" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog is blue.[(triple1)] @1: The dog is big.[(((triple1) -> rule1))] @2: The dog is nice.[(((triple1 ((triple1) -> rule1)) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
((triple1) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2