Anne is furry. Anne is green. Anne is round. Anne is young. Charlie is smart. Fiona is big. Fiona is green. Fiona is quiet. Fiona is not round. Fiona is smart. Harry is green. Harry is quiet. If someone is round then they are big. Big, green people are young. If someone is big and not smart then they are young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Big, green people are young.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is big and not smart then they are young.
((("someone" "is" "big" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "young" "+"))
Anne is young.
True
1
proof
[(triple4 OR ((((triple3) -> rule1) triple2) -> rule2))]
("Anne" "is" "young" "+")
triple4
((((triple3) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Fiona is not smart.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "smart" "-")
triple10
Anne is big.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is not young.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("Fiona" "is" "young" "-")
((triple6 triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "big" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is round.[(triple3)] Anne is young.[(triple4 OR ((((triple3) -> rule1) triple2) -> rule2))] Charlie is smart.[(triple5)] Fiona is big.[(triple6)] Fiona is green.[(triple7)] Fiona is not round.[(triple9)] Fiona is quiet.[(triple8)] Fiona is smart.[(triple10)] Harry is green.[(triple11)] Harry is quiet.[(triple12)] @1: Anne is big.[(((triple3) -> rule1))] Fiona is young.[(((triple6 triple7) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((((triple3) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is not round.
("Fiona" "is" "round" "-")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6 triple7) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1