The dog is not big. The dog is blue. The dog is cold. The dog is green. The dog is kind. If something is green then it is cold. Blue, kind things are cold. If something is green then it is blue.
The dog is not big.
("dog" "is" "big" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
If something is green then it is cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Blue, kind things are cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
The dog is kind.
True
1
proof
[(triple5)]
("dog" "is" "kind" "+")
triple5
The dog is not cold.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule1) OR ((triple2 triple5) -> rule2) OR ((((triple4) -> rule3) triple5) -> rule2))]
("dog" "is" "cold" "-")
triple3
((triple4) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((triple2 triple5) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is blue.[(triple2 OR ((triple4) -> rule3))] The dog is cold.[(triple3 OR ((triple4) -> rule1) OR ((triple2 triple5) -> rule2) OR ((((triple4) -> rule3) triple5) -> rule2))] The dog is green.[(triple4)] The dog is kind.[(triple5)] The dog is not big.[(triple1)]
The dog is blue.
("dog" "is" "blue" "+")
triple2
((triple4) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
triple3
((triple4) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((triple2 triple5) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is green.
("dog" "is" "green" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is not big.
("dog" "is" "big" "-")
triple1