Charlie is cold. Charlie is nice. Erin is rough. Erin is round. Gary is rough. Gary is round. Gary is smart. Round people are nice. If someone is green then they are nice. Nice people are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Gary is rough.
True
1
proof
[(triple5)]
("Gary" "is" "rough" "+")
triple5
Gary is not rough.
False
1
inv-proof
[(triple5)]
("Gary" "is" "rough" "-")
triple5
Charlie is green.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "green" "+")
((triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "nice" "-")
((triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is green.
True
3
proof
[(((((triple6) -> rule1)) -> rule3))]
("Gary" "is" "green" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule3))]
("Gary" "is" "green" "-")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Charlie is cold.[(triple1)] Charlie is nice.[(triple2)] Erin is rough.[(triple3)] Erin is round.[(triple4)] Gary is rough.[(triple5)] Gary is round.[(triple6)] Gary is smart.[(triple7)] @1: Charlie is green.[(((triple2) -> rule3))] Erin is nice.[(((triple4) -> rule1))] Gary is nice.[(((triple6) -> rule1))] @2: Erin is green.[(((((triple4) -> rule1)) -> rule3))] Gary is green.[(((((triple6) -> rule1)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2