The dog is big. The dog is blue. The dog is cold. The dog is green. The dog is red. All green people are big. If someone is big and cold then they are green. If someone is big and red then they are blue.
The dog is 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 red.
("dog" "is" "red" "+")
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is big and cold then they are green.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is big and red then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
The dog is blue.
True
1
proof
[(triple2 OR ((triple1 triple5) -> rule3) OR ((((triple4) -> rule1) triple5) -> rule3))]
("dog" "is" "blue" "+")
triple2
((triple1 triple5) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not big.
False
1
inv-proof
[(triple1 OR ((triple4) -> rule1))]
("dog" "is" "big" "-")
triple1
((triple4) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "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 big.[(triple1 OR ((triple4) -> rule1))] The dog is blue.[(triple2 OR ((triple1 triple5) -> rule3) OR ((((triple4) -> rule1) triple5) -> rule3))] The dog is cold.[(triple3)] The dog is green.[(triple4 OR ((triple1 triple3) -> rule2))] The dog is red.[(triple5)]
The dog is big.
("dog" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
triple2
((triple1 triple5) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
((triple1 triple3) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is red.
("dog" "is" "red" "+")
triple5