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