Charlie is big. Charlie is furry. Charlie is young. Erin is big. Erin is furry. Erin is green. Erin is kind. Erin is red. Erin is round. Erin is young. Harry is big. Harry is furry. Harry is red. Harry is round. Harry is young. Kind, big people are red. If someone is kind and big then they are young. Young people are kind.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind, big people are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is kind and big then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Harry is red.
True
1
proof
[(triple13 OR ((((triple15) -> rule3) triple11) -> rule1))]
("Harry" "is" "red" "+")
triple13
((((triple15) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Charlie is kind.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple15) -> rule3))]
("Harry" "is" "kind" "-")
((triple15) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is red.
True
4
proof
[(((((triple3) -> rule3) triple1) -> rule1))]
("Charlie" "is" "red" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple3) -> rule3) triple1) -> rule1))]
("Charlie" "is" "red" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is young.[(triple3)] Erin is big.[(triple4)] Erin is furry.[(triple5)] Erin is green.[(triple6)] Erin is kind.[(triple7 OR ((triple10) -> rule3))] Erin is red.[(triple8 OR ((triple7 triple4) -> rule1) OR ((((triple10) -> rule3) triple4) -> rule1))] Erin is round.[(triple9)] Erin is young.[(triple10 OR ((triple7 triple4) -> rule2))] Harry is big.[(triple11)] Harry is furry.[(triple12)] Harry is red.[(triple13 OR ((((triple15) -> rule3) triple11) -> rule1))] Harry is round.[(triple14)] Harry is young.[(triple15)] @1: Charlie is kind.[(((triple3) -> rule3))] Harry is kind.[(((triple15) -> rule3))] @2: Charlie is red.[(((((triple3) -> rule3) triple1) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
((triple10) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
triple8
((triple7 triple4) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple10) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
((triple7 triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((((triple15) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple15) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2