Charlie is big. Charlie is kind. Charlie is nice. Erin is big. Erin is kind. Erin is red. Erin is rough. Erin is young. Gary is kind. Gary is red. If someone is big then they are young. All rough, cold people are nice. All kind people are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All rough, cold people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Charlie is kind.
True
1
proof
[(triple2)]
("Charlie" "is" "kind" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple7)]
("Erin" "is" "rough" "-")
triple7
Gary is big.
True
2
proof
[(((triple9) -> rule3))]
("Gary" "is" "big" "+")
((triple9) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "young" "-")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is big.[(triple1 OR ((triple2) -> rule3))] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Erin is big.[(triple4 OR ((triple5) -> rule3))] Erin is kind.[(triple5)] Erin is red.[(triple6)] Erin is rough.[(triple7)] Erin is young.[(triple8 OR ((triple4) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Gary is kind.[(triple9)] Gary is red.[(triple10)] @1: Charlie is young.[(((triple1) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] Gary is big.[(((triple9) -> rule3))] @2: Gary is young.[(((((triple9) -> rule3)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple5) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
triple8
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Gary is red.
("Gary" "is" "red" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple9) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2