The bald eagle is big. The bald eagle is red. The bald eagle is rough. If something is rough then it is red. All big, nice things are rough. Red things are big. If the bald eagle is rough then the bald eagle is red. All young things are big. Young things are big. If the bald eagle is red then the bald eagle is young. Nice, red things are young.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All big, nice things are rough.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If the bald eagle is rough then the bald eagle is red.
((("bald eagle" "is" "rough" "+")) -> ("bald eagle" "is" "red" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If the bald eagle is red then the bald eagle is young.
((("bald eagle" "is" "red" "+")) -> ("bald eagle" "is" "young" "+"))
Nice, red things are young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
The bald eagle is big.
True
1
proof
[(triple1 OR ((triple2) -> rule3) OR ((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule7)) -> rule6) OR ((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule7)) -> rule5) OR ((((((triple3) -> rule1)) -> rule7)) -> rule6) OR ((((((triple3) -> rule4)) -> rule7)) -> rule5) OR ((((((triple3) -> rule4)) -> rule7)) -> rule6))]
("bald eagle" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle is not red.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule1) OR ((triple3) -> rule4))]
("bald eagle" "is" "red" "-")
triple2
((triple3) -> (rule1 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
((triple3) -> (rule4 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle does not need the bald eagle.
Unknown
inv-random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle is big.[(triple1 OR ((triple2) -> rule3) OR ((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule7)) -> rule6) OR ((((triple3) -> rule1)) -> rule3) OR ((((triple3) -> rule4)) -> rule3) OR ((((((triple3) -> rule1)) -> rule7)) -> rule5) OR ((((((triple3) -> rule1)) -> rule7)) -> rule6) OR ((((((triple3) -> rule4)) -> rule7)) -> rule5) OR ((((((triple3) -> rule4)) -> rule7)) -> rule6))] The bald eagle is red.[(triple2 OR ((triple3) -> rule1) OR ((triple3) -> rule4))] The bald eagle is rough.[(triple3)] @1: The bald eagle is young.[(((triple2) -> rule7) OR ((((triple3) -> rule1)) -> rule7) OR ((((triple3) -> rule4)) -> rule7))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is big.
("bald eagle" "is" "big" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple2
((triple3) -> (rule1 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
((triple3) -> (rule4 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple3
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple2) -> (rule7 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2