The dog is big. The dog is cold. The dog is red. The dog is round. The dog is young. All red people are big. All round people are big. If someone is red then they are cold. If someone is cold and red then they are round. If the dog is red and the dog is cold then the dog is round. If the dog is round then the dog is red.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and red then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If the dog is red and the dog is cold then the dog is round.
((("dog" "is" "red" "+") ("dog" "is" "cold" "+")) -> ("dog" "is" "round" "+"))
If the dog is round then the dog is red.
((("dog" "is" "round" "+")) -> ("dog" "is" "red" "+"))
The dog is round.
True
1
proof
[(triple4 OR ((triple2 triple3) -> rule4) OR ((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule3) triple3) -> rule4))]
("dog" "is" "round" "+")
triple4
((triple2 triple3) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple3 triple2) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is not red.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule6))]
("dog" "is" "red" "-")
triple3
((triple4) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog is big.[(triple1 OR ((triple3) -> rule1) OR ((triple4) -> rule2) OR ((((triple4) -> rule6)) -> rule1) OR ((((triple2 triple3) -> rule4)) -> rule2) OR ((((triple3 triple2) -> rule5)) -> rule2) OR ((((triple3 ((triple3) -> rule3)) -> rule5)) -> rule2) OR ((((((triple3) -> rule3) triple3) -> rule4)) -> rule2))] The dog is cold.[(triple2 OR ((triple3) -> rule3) OR ((((triple4) -> rule6)) -> rule3))] The dog is red.[(triple3 OR ((triple4) -> rule6))] The dog is round.[(triple4 OR ((triple2 triple3) -> rule4) OR ((triple3 triple2) -> rule5) OR ((triple3 ((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule3) triple3) -> rule4))] The dog is young.[(triple5)]
The dog is big.
("dog" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
((triple4) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
((((triple2 triple3) -> (rule4 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
((((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
((((((triple3) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog is cold.
("dog" "is" "cold" "+")
triple2
((triple3) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is red.
("dog" "is" "red" "+")
triple3
((triple4) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple4
((triple2 triple3) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple3 triple2) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((triple3 ((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog is young.
("dog" "is" "young" "+")
triple5