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