Charlie is kind. Erin is not kind. Gary is young. Harry is big. If someone is kind and rough then they are smart. If Erin is kind then Erin is not big. Big people are nice. If someone is red then they are not nice. If someone is big then they are not kind. Kind people are rough.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is kind and rough then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Erin is kind then Erin is not big.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "big" "-"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are not nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If someone is big then they are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Erin is not kind.
True
1
proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is kind.
False
2
inv-proof
[(((triple4) -> rule5))]
("Harry" "is" "kind" "+")
((triple4) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Charlie is smart.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule1))]
("Charlie" "is" "smart" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule1))]
("Charlie" "is" "smart" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is kind.[(triple1)] Erin is not kind.[(triple2)] Gary is young.[(triple3)] Harry is big.[(triple4)] @1: Charlie is rough.[(((triple1) -> rule6))] Harry is nice.[(((triple4) -> rule3))] Harry is not kind.[(((triple4) -> rule5))] @2: Charlie is smart.[(((triple1 ((triple1) -> rule6)) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is not kind.
("Erin" "is" "kind" "-")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
((triple4) -> (rule5 % int1))
Harry is not kind.
("Harry" "is" "kind" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2