Anne is nice. Anne is not quiet. Anne is young. Fiona is furry. Fiona is quiet. Fiona is young. Gary is big. Gary is round. Harry is not quiet. Harry is round. If Harry is white then Harry is round. If Harry is big then Harry is young. All round people are big.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is young.
("Anne" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is round.
("Harry" "is" "round" "+")
If Harry is white then Harry is round.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "+"))
If Harry is big then Harry is young.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "young" "+"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule3))]
("Gary" "is" "big" "-")
triple7
((triple8) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is big.
True
2
proof
[(((triple10) -> rule3))]
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple10) -> rule3))]
("Harry" "is" "big" "-")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
True
3
proof
[(((((triple10) -> rule3)) -> rule2))]
("Harry" "is" "young" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule2))]
("Harry" "is" "young" "-")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Anne is not quiet.[(triple2)] Anne is young.[(triple3)] Fiona is furry.[(triple4)] Fiona is quiet.[(triple5)] Fiona is young.[(triple6)] Gary is big.[(triple7 OR ((triple8) -> rule3))] Gary is round.[(triple8)] Harry is not quiet.[(triple9)] Harry is round.[(triple10)] @1: Harry is big.[(((triple10) -> rule3))] @2: Harry is young.[(((((triple10) -> rule3)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple8) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple8
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2