Harry is big. Harry is kind. Harry is round. If someone is red and round then they are green. If someone is young then they are round. If someone is young and big then they are green. Big people are young. Blue, young people are green. All blue, round people are young. Red people are big. If someone is round and young then they are green.
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is red and round then they are green.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is young and big then they are green.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Blue, young people are green.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
All blue, round people are young.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is round and young then they are green.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Harry is kind.
True
1
proof
[(triple2)]
("Harry" "is" "kind" "+")
triple2
Harry is not kind.
False
1
inv-proof
[(triple2)]
("Harry" "is" "kind" "-")
triple2
Harry is young.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "young" "+")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "young" "-")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
True
4
proof
[(((triple3 ((triple1) -> rule4)) -> rule8) OR ((((triple1) -> rule4) triple1) -> rule3) OR ((((((triple1) -> rule4)) -> rule2) ((triple1) -> rule4)) -> rule8))]
("Harry" "is" "green" "+")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple1) -> (rule4 % int3))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not green.
False
4
inv-proof
[(((triple3 ((triple1) -> rule4)) -> rule8) OR ((((triple1) -> rule4) triple1) -> rule3) OR ((((((triple1) -> rule4)) -> rule2) ((triple1) -> rule4)) -> rule8))]
("Harry" "is" "green" "-")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple1) -> (rule4 % int3))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Harry is big.[(triple1)] Harry is kind.[(triple2)] Harry is round.[(triple3 OR ((((triple1) -> rule4)) -> rule2))] @1: Harry is young.[(((triple1) -> rule4))] @2: Harry is green.[(((triple3 ((triple1) -> rule4)) -> rule8) OR ((((triple1) -> rule4) triple1) -> rule3) OR ((((((triple1) -> rule4)) -> rule2) ((triple1) -> rule4)) -> rule8))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple1) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple1) -> (rule4 % int3))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3