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