Charlie is nice. Charlie is rough. Charlie is young. Erin is big. Erin is furry. Erin is nice. Erin is quiet. Harry is furry. Harry is rough. Harry is young. All rough things are nice. Quiet, young things are big. All furry, nice things are big.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Quiet, young things are big.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All furry, nice things are big.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Erin is big.
True
1
proof
[(triple4 OR ((triple5 triple6) -> rule3))]
("Erin" "is" "big" "+")
triple4
((triple5 triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not nice.
False
1
inv-proof
[(triple6)]
("Erin" "is" "nice" "-")
triple6
Harry is nice.
True
2
proof
[(((triple9) -> rule1))]
("Harry" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple9) -> rule1))]
("Harry" "is" "nice" "-")
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
True
4
proof
[(((triple8 ((triple9) -> rule1)) -> rule3))]
("Harry" "is" "big" "+")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple8 ((triple9) -> rule1)) -> rule3))]
("Harry" "is" "big" "-")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Charlie is nice.[(triple1 OR ((triple2) -> rule1))] Charlie is rough.[(triple2)] Charlie is young.[(triple3)] Erin is big.[(triple4 OR ((triple5 triple6) -> rule3))] Erin is furry.[(triple5)] Erin is nice.[(triple6)] Erin is quiet.[(triple7)] Harry is furry.[(triple8)] Harry is rough.[(triple9)] Harry is young.[(triple10)] @1: Harry is nice.[(((triple9) -> rule1))] @2: Harry is big.[(((triple8 ((triple9) -> rule1)) -> rule3))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
((triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
((triple5 triple6) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple8 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2