Anne is round. Dave is furry. Gary is round. Harry is not round. Furry things are young. Big things are smart. If something is smart and not rough then it is big. All furry, young things are big. If something is furry and not round then it is big. If something is smart and not young then it is big.
Anne is round.
("Anne" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not round.
("Harry" "is" "round" "-")
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is smart and not rough then it is big.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "+"))
All furry, young things are big.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is furry and not round then it is big.
((("something" "is" "furry" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
If something is smart and not young then it is big.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "+"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Gary is not round.
False
1
inv-proof
[(triple3)]
("Gary" "is" "round" "-")
triple3
Dave is young.
True
2
proof
[(((triple2) -> rule1))]
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "young" "-")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule4))]
("Dave" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule4))]
("Dave" "is" "big" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
True
5
proof
[(((((triple2 ((triple2) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "smart" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule1)) -> rule4)) -> rule2))]
("Dave" "is" "smart" "-")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "smart" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is round.[(triple1)] Dave is furry.[(triple2)] Gary is round.[(triple3)] Harry is not round.[(triple4)] @1: Dave is young.[(((triple2) -> rule1))] @2: Dave is big.[(((triple2 ((triple2) -> rule1)) -> rule4))] @3: Dave is smart.[(((((triple2 ((triple2) -> rule1)) -> rule4)) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Harry is not round.
("Harry" "is" "round" "-")
triple4
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2 ((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3