Charlie is green. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is young. Dave is green. Dave is nice. Dave is rough. Dave is round. If something is nice and not quiet then it is smart. If something is green then it is smart. If something is smart and nice then it is young.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
If something is nice and not quiet then it is smart.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "smart" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is smart and nice then it is young.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Charlie is quiet.
True
1
proof
[(triple3)]
("Charlie" "is" "quiet" "+")
triple3
Charlie is not young.
False
1
inv-proof
[(triple6 OR ((triple5 triple2) -> rule3) OR ((((triple1) -> rule2) triple2) -> rule3))]
("Charlie" "is" "young" "-")
triple6
((triple5 triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is smart.
True
2
proof
[(((triple7) -> rule2))]
("Dave" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple7) -> rule2))]
("Dave" "is" "smart" "-")
((triple7) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
True
4
proof
[(((((triple7) -> rule2) triple8) -> rule3))]
("Dave" "is" "young" "+")
((((triple7) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple7) -> rule2) triple8) -> rule3))]
("Dave" "is" "young" "-")
((((triple7) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Charlie is smart.[(triple5 OR ((triple1) -> rule2))] Charlie is young.[(triple6 OR ((triple5 triple2) -> rule3) OR ((((triple1) -> rule2) triple2) -> rule3))] Dave is green.[(triple7)] Dave is nice.[(triple8)] Dave is rough.[(triple9)] Dave is round.[(triple10)] @1: Dave is smart.[(((triple7) -> rule2))] @2: Dave is young.[(((((triple7) -> rule2) triple8) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple5 triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple7) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2