Charlie is big. Charlie is round. Charlie is young. Harry is big. Harry is blue. Harry is nice. Harry is quiet. Harry is rough. Harry is round. Harry is young. If someone is quiet then they are blue. Big, round people are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Big, round people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not young.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "young" "-")
triple3
Charlie is quiet.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple1 triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule1))]
("Charlie" "is" "blue" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is big.[(triple1)] Charlie is round.[(triple2)] Charlie is young.[(triple3)] Harry is big.[(triple4)] Harry is blue.[(triple5 OR ((triple7) -> rule1) OR ((((triple4 triple9) -> rule2)) -> rule1))] Harry is nice.[(triple6)] Harry is quiet.[(triple7 OR ((triple4 triple9) -> rule2))] Harry is rough.[(triple8)] Harry is round.[(triple9)] Harry is young.[(triple10)] @1: Charlie is quiet.[(((triple1 triple2) -> rule2))] @2: Charlie is blue.[(((((triple1 triple2) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple4 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((triple4 triple9) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2