Anne is big. Anne is young. Charlie is big. Charlie is green. Charlie is round. Dave is big. Dave is round. If someone is young then they are big. All big, young people are round. All kind people are young.
Anne is big.
("Anne" "is" "big" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All big, young people are round.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Dave is round.
True
1
proof
[(triple7)]
("Dave" "is" "round" "+")
triple7
Charlie is not round.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "round" "-")
triple5
Anne is round.
True
3
proof
[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
("Anne" "is" "round" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not round.
False
3
inv-proof
[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
("Anne" "is" "round" "-")
((triple1 triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule1))] Anne is young.[(triple2)] Charlie is big.[(triple3)] Charlie is green.[(triple4)] Charlie is round.[(triple5)] Dave is big.[(triple6)] Dave is round.[(triple7)] @1: Anne is round.[(((triple1 triple2) -> rule2) OR ((((triple2) -> rule1) triple2) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1 triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2