Charlie is cold. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is young. Erin is cold. Erin is kind. Erin is quiet. Erin is rough. Erin is round. Erin is young. Gary is cold. Gary is quiet. Gary is white. Gary is young. Quiet people are white. If someone is white then they are round.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Erin is young.
True
1
proof
[(triple12)]
("Erin" "is" "young" "+")
triple12
Erin is not round.
False
1
inv-proof
[(triple11 OR ((((triple9) -> rule1)) -> rule2))]
("Erin" "is" "round" "-")
triple11
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Gary is round.
True
2
proof
[(((triple15) -> rule2) OR ((((triple14) -> rule1)) -> rule2))]
("Gary" "is" "round" "+")
((triple15) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Charlie is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "white" "-")
((triple3) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Charlie is cold.[(triple1)] Charlie is kind.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Charlie is round.[(triple5 OR ((((triple3) -> rule1)) -> rule2))] Charlie is young.[(triple6)] Erin is cold.[(triple7)] Erin is kind.[(triple8)] Erin is quiet.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11 OR ((((triple9) -> rule1)) -> rule2))] Erin is young.[(triple12)] Gary is cold.[(triple13)] Gary is quiet.[(triple14)] Gary is white.[(triple15 OR ((triple14) -> rule1))] Gary is young.[(triple16)] @1: Charlie is white.[(((triple3) -> rule1))] Erin is white.[(((triple9) -> rule1))] Gary is round.[(((triple15) -> rule2) OR ((((triple14) -> rule1)) -> rule2))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple12
Gary is cold.
("Gary" "is" "cold" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is white.
("Gary" "is" "white" "+")
triple15
((triple14) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple16
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple9) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple15) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2