Dave is quiet. Gary is rough. Harry is nice. Nice things are not smart. If Dave is quiet then Dave is green. Nice things are young. If something is quiet then it is rough. Young, quiet things are rough. Quiet, young things are not green. Nice, young things are quiet. If Gary is green then Gary is nice.
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Nice things are not smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "-"))
If Dave is quiet then Dave is green.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "green" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Young, quiet things are rough.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Quiet, young things are not green.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
Nice, young things are quiet.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If Gary is green then Gary is nice.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "nice" "+"))
Gary is rough.
True
1
proof
[(triple2)]
("Gary" "is" "rough" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple3)]
("Harry" "is" "nice" "-")
triple3
Harry is not smart.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is quiet.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule7))]
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not quiet.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule7))]
("Harry" "is" "quiet" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is young.
Unknown
rconc
[@2: Gary is young.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Gary" "is" "quiet" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Dave is quiet.[(triple1)] Gary is rough.[(triple2)] Harry is nice.[(triple3)] @1: Dave is green.[(((triple1) -> rule2))] Dave is rough.[(((triple1) -> rule4))] Harry is not smart.[(((triple3) -> rule1))] Harry is young.[(((triple3) -> rule3))] @2: Harry is quiet.[(((triple3 ((triple3) -> rule3)) -> rule7))] @3: Harry is not green.[(((((triple3 ((triple3) -> rule3)) -> rule7) ((triple3) -> rule3)) -> rule6))] Harry is rough.[(((((triple3 ((triple3) -> rule3)) -> rule7)) -> rule4) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule3)) -> rule7)) -> rule5))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule7 % int2)) ((triple3) -> (rule3 % int3))) -> (rule6 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3