Charlie is big. Charlie is rough. Charlie is smart. Dave is furry. Dave is quiet. Harry is big. Harry is furry. Harry is not green. Harry is not red. Harry is smart. Quiet, green things are not smart. Big things are rough. All rough things are not quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is not red.
("Harry" "is" "red" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet, green things are not smart.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
Big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All rough things are not quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is not quiet.
True
2
proof
[(((triple2) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Harry is not rough.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "rough" "-")
((triple6) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not quiet.
True
3
proof
[(((((triple6) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule3))]
("Harry" "is" "quiet" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is big.[(triple1)] Charlie is rough.[(triple2 OR ((triple1) -> rule2))] Charlie is smart.[(triple3)] Dave is furry.[(triple4)] Dave is quiet.[(triple5)] Harry is big.[(triple6)] Harry is furry.[(triple7)] Harry is not green.[(triple8)] Harry is not red.[(triple9)] Harry is smart.[(triple10)] @1: Charlie is not quiet.[(((triple2) -> rule3) OR ((((triple1) -> rule2)) -> rule3))] Harry is rough.[(((triple6) -> rule2))] @2: Harry is not quiet.[(((((triple6) -> rule2)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is not green.
("Harry" "is" "green" "-")
triple8
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2