Charlie is big. Charlie is not cold. Charlie is rough. Charlie is smart. Charlie is white. Erin is nice. Erin is round. Erin is smart. Erin is white. Gary is cold. Gary is nice. Gary is round. Gary is not smart. Harry is nice. Harry is not rough. Harry is round. If Gary is cold then Gary is not rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
If Gary is cold then Gary is not rough.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "rough" "-"))
Harry is not rough.
True
1
proof
[(triple15)]
("Harry" "is" "rough" "-")
triple15
Erin is not nice.
False
1
inv-proof
[(triple6)]
("Erin" "is" "nice" "-")
triple6
Gary is not rough.
True
2
proof
[(((triple10) -> rule1))]
("Gary" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("Gary" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Charlie is big.[(triple1)] Charlie is not cold.[(triple2)] Charlie is rough.[(triple3)] Charlie is smart.[(triple4)] Charlie is white.[(triple5)] Erin is nice.[(triple6)] Erin is round.[(triple7)] Erin is smart.[(triple8)] Erin is white.[(triple9)] Gary is cold.[(triple10)] Gary is nice.[(triple11)] Gary is not smart.[(triple13)] Gary is round.[(triple12)] Harry is nice.[(triple14)] Harry is not rough.[(triple15)] Harry is round.[(triple16)] @1: Gary is not rough.[(((triple10) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is not smart.
("Gary" "is" "smart" "-")
triple13
Gary is round.
("Gary" "is" "round" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is not rough.
("Harry" "is" "rough" "-")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Gary is not rough.
("Gary" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1