Charlie is big. Dave is green. Dave is nice. Dave is round. Fiona is not big. Fiona is kind. Fiona is nice. Fiona is not young. Harry is big. Harry is round. If Harry is nice and Harry is round then Harry is not green. If Harry is young and Harry is round then Harry is nice. If Harry is round then Harry is young.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is nice and Harry is round then Harry is not green.
((("Harry" "is" "nice" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "green" "-"))
If Harry is young and Harry is round then Harry is nice.
((("Harry" "is" "young" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "nice" "+"))
If Harry is round then Harry is young.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "young" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Harry is young.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "young" "+")
((triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple10) -> rule3))]
("Harry" "is" "young" "-")
((triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "nice" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "nice" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not green.
True
6
proof
[(((((((triple10) -> rule3) triple10) -> rule2) triple10) -> rule1))]
("Harry" "is" "green" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is green.
False
6
inv-proof
[(((((((triple10) -> rule3) triple10) -> rule2) triple10) -> rule1))]
("Harry" "is" "green" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Dave is green.[(triple2)] Dave is nice.[(triple3)] Dave is round.[(triple4)] Fiona is kind.[(triple6)] Fiona is nice.[(triple7)] Fiona is not big.[(triple5)] Fiona is not young.[(triple8)] Harry is big.[(triple9)] Harry is round.[(triple10)] @1: Harry is young.[(((triple10) -> rule3))] @2: Harry is nice.[(((((triple10) -> rule3) triple10) -> rule2))] @3: Harry is not green.[(((((((triple10) -> rule3) triple10) -> rule2) triple10) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is not big.
("Fiona" "is" "big" "-")
triple5
Fiona is not young.
("Fiona" "is" "young" "-")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3