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