Charlie is big. Harry is rough. If someone is quiet then they are blue. If Charlie is big then Charlie is round. If Charlie is young then Charlie is kind. If someone is round then they are young. If someone is round and big then they are rough. If Charlie is kind then Charlie is young.
Charlie is big.
("Charlie" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is big then Charlie is round.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "round" "+"))
If Charlie is young then Charlie is kind.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "kind" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is round and big then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is kind then Charlie is young.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "young" "+"))
Harry is rough.
True
1
proof
[(triple2)]
("Harry" "is" "rough" "+")
triple2
Harry is not rough.
False
1
inv-proof
[(triple2)]
("Harry" "is" "rough" "-")
triple2
Charlie is round.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "round" "-")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Harry is rough.[(triple2)] @1: Charlie is round.[(((triple1) -> rule2))] @2: Charlie is rough.[(((((triple1) -> rule2) triple1) -> rule5))] Charlie is young.[(((((triple1) -> rule2)) -> rule4))] @3: Charlie is kind.[(((((((triple1) -> rule2)) -> rule4)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Harry is rough.
("Harry" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3