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