Anne is big. Anne is kind. Anne is nice. Anne is round. Dave is big. Dave is nice. Dave is rough. Dave is young. Harry is round. Harry is smart. If someone is round and young then they are rough. All nice people are young. Rough people are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is round and young then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Anne is round.
True
1
proof
[(triple4)]
("Anne" "is" "round" "+")
triple4
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Anne is young.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "young" "+")
((triple3) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple7) -> rule3))]
("Dave" "is" "smart" "-")
((triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is rough.
True
4
proof
[(((triple4 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "rough" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple4 ((triple3) -> rule2)) -> rule1))]
("Anne" "is" "rough" "-")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
True
5
proof
[(((((triple4 ((triple3) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "smart" "+")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not smart.
False
5
inv-proof
[(((((triple4 ((triple3) -> rule2)) -> rule1)) -> rule3))]
("Anne" "is" "smart" "-")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- 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 big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is round.[(triple4)] Dave is big.[(triple5)] Dave is nice.[(triple6)] Dave is rough.[(triple7)] Dave is young.[(triple8 OR ((triple6) -> rule2))] Harry is round.[(triple9)] Harry is smart.[(triple10)] @1: Anne is young.[(((triple3) -> rule2))] Dave is smart.[(((triple7) -> rule3))] @2: Anne is rough.[(((triple4 ((triple3) -> rule2)) -> rule1))] @3: Anne is smart.[(((((triple4 ((triple3) -> rule2)) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple6) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple4 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((triple4 ((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3