Bob is big. Bob is nice. Bob is rough. Bob is smart. Bob is young. Charlie is green. Charlie is nice. Charlie is red. Charlie is rough. Charlie is young. If something is red and big then it is smart. All red, young things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If something is red and big then it is smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All red, young things are big.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "green" "-")
triple6
Charlie is big.
True
3
proof
[(((triple8 triple10) -> rule2))]
("Charlie" "is" "big" "+")
((triple8 triple10) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
3
inv-proof
[(((triple8 triple10) -> rule2))]
("Charlie" "is" "big" "-")
((triple8 triple10) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
True
5
proof
[(((triple8 ((triple8 triple10) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
((triple8 ((triple8 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not smart.
False
5
inv-proof
[(((triple8 ((triple8 triple10) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "-")
((triple8 ((triple8 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is rough.[(triple3)] Bob is smart.[(triple4)] Bob is young.[(triple5)] Charlie is green.[(triple6)] Charlie is nice.[(triple7)] Charlie is red.[(triple8)] Charlie is rough.[(triple9)] Charlie is young.[(triple10)] @1: Charlie is big.[(((triple8 triple10) -> rule2))] @2: Charlie is smart.[(((triple8 ((triple8 triple10) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
Charlie is rough.
("Charlie" "is" "rough" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Charlie is big.
("Charlie" "is" "big" "+")
((triple8 triple10) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8 ((triple8 triple10) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2