Bob is big. Bob is furry. Bob is green. Bob is kind. Bob is nice. Bob is red. Bob is rough. Charlie is big. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is red. Charlie is rough. Dave is big. Dave is red. All rough people are kind. All big people are rough.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple16)]
("Dave" "is" "red" "-")
triple16
Dave is rough.
True
2
proof
[(((triple15) -> rule2))]
("Dave" "is" "rough" "+")
((triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple15) -> rule2))]
("Dave" "is" "rough" "-")
((triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
True
3
proof
[(((((triple15) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple15) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is kind.[(triple4 OR ((triple7) -> rule1) OR ((((triple1) -> rule2)) -> rule1))] Bob is nice.[(triple5)] Bob is red.[(triple6)] Bob is rough.[(triple7 OR ((triple1) -> rule2))] Charlie is big.[(triple8)] Charlie is furry.[(triple9)] Charlie is green.[(triple10)] Charlie is kind.[(triple11 OR ((triple14) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Charlie is nice.[(triple12)] Charlie is red.[(triple13)] Charlie is rough.[(triple14 OR ((triple8) -> rule2))] Dave is big.[(triple15)] Dave is red.[(triple16)] @1: Dave is rough.[(((triple15) -> rule2))] @2: Dave is kind.[(((((triple15) -> rule2)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple7) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is rough.
("Bob" "is" "rough" "+")
triple7
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
((triple14) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
triple13
Charlie is rough.
("Charlie" "is" "rough" "+")
triple14
((triple8) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple15
Dave is red.
("Dave" "is" "red" "+")
triple16
Dave is rough.
("Dave" "is" "rough" "+")
((triple15) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2