Bob is quiet. Bob is rough. Bob is smart. Bob is white. Bob is young. Dave is blue. Dave is rough. Dave is white. Gary is not big. Gary is blue. Gary is rough. Gary is white. Smart people are rough. If someone is blue and white then they are not young. All young people are not big.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and white then they are not young.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "-"))
All young people are not big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "-"))
Bob is rough.
True
1
proof
[(triple2 OR ((triple3) -> rule1))]
("Bob" "is" "rough" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple12)]
("Gary" "is" "white" "-")
triple12
Bob is not big.
True
2
proof
[(((triple5) -> rule3))]
("Bob" "is" "big" "-")
((triple5) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is big.
False
2
inv-proof
[(((triple5) -> rule3))]
("Bob" "is" "big" "+")
((triple5) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is quiet.[(triple1)] Bob is rough.[(triple2 OR ((triple3) -> rule1))] Bob is smart.[(triple3)] Bob is white.[(triple4)] Bob is young.[(triple5)] Dave is blue.[(triple6)] Dave is rough.[(triple7)] Dave is white.[(triple8)] Gary is blue.[(triple10)] Gary is not big.[(triple9)] Gary is rough.[(triple11)] Gary is white.[(triple12)] @1: Bob is not big.[(((triple5) -> rule3))] Dave is not young.[(((triple6 triple8) -> rule2))] Gary is not young.[(((triple10 triple12) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is not big.
("Gary" "is" "big" "-")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Bob is not big.
("Bob" "is" "big" "-")
((triple5) -> (rule3 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple6 triple8) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Gary is not young.
("Gary" "is" "young" "-")
((triple10 triple12) -> (rule2 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1