Anne is rough. Bob is young. Charlie is round. Harry is blue. If someone is nice then they are rough. All round, big people are blue. Rough, big people are nice. Rough people are kind. Round people are blue. Blue people are rough. All blue people are young. If someone is kind then they are nice.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All round, big people are blue.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Rough, big people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Charlie is blue.
True
2
proof
[(((triple3) -> rule5))]
("Charlie" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "young" "-")
((triple4) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Charlie is young.
True
3
proof
[(((((triple3) -> rule5)) -> rule7))]
("Charlie" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4))]
("Harry" "is" "kind" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Charlie is kind.
True
4
proof
[(((((((triple3) -> rule5)) -> rule6)) -> rule4))]
("Charlie" "is" "kind" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule8))]
("Harry" "is" "nice" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is nice.
Unknown
rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is blue.
Unknown
rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is rough.[(triple1)] Bob is young.[(triple2)] Charlie is round.[(triple3)] Harry is blue.[(triple4)] @1: Anne is kind.[(((triple1) -> rule4))] Charlie is blue.[(((triple3) -> rule5))] Harry is rough.[(((triple4) -> rule6))] Harry is young.[(((triple4) -> rule7))] @2: Anne is nice.[(((((triple1) -> rule4)) -> rule8))] Charlie is rough.[(((((triple3) -> rule5)) -> rule6))] Charlie is young.[(((((triple3) -> rule5)) -> rule7))] Harry is kind.[(((((triple4) -> rule6)) -> rule4))] @3: Charlie is kind.[(((((((triple3) -> rule5)) -> rule6)) -> rule4))] Harry is nice.[(((((((triple4) -> rule6)) -> rule4)) -> rule8))] @4: Charlie is nice.[(((((((((triple3) -> rule5)) -> rule6)) -> rule4)) -> rule8))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4