Anne is blue. Anne is nice. Anne is rough. Charlie is blue. Charlie is nice. Charlie is rough. Charlie is not round. Erin is furry. Erin is not round. Harry is big. Harry is blue. Harry is furry. Harry is nice. Harry is rough. Harry is round. If someone is round and not nice then they are not big. Nice people are big. If someone is big and not round then they are not furry. Round people are blue. If someone is round and not blue then they are young. If someone is furry and not rough then they are not young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not round.
("Erin" "is" "round" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is round and not nice then they are not big.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "-"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is big and not round then they are not furry.
((("someone" "is" "big" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "furry" "-"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and not blue then they are young.
((("someone" "is" "round" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
If someone is furry and not rough then they are not young.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "-"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "-")
triple5
Charlie is big.
True
2
proof
[(((triple5) -> rule2))]
("Charlie" "is" "big" "+")
((triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple5) -> rule2))]
("Charlie" "is" "big" "-")
((triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not furry.
True
4
proof
[(((((triple5) -> rule2) triple7) -> rule3))]
("Charlie" "is" "furry" "-")
((((triple5) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
False
4
inv-proof
[(((((triple5) -> rule2) triple7) -> rule3))]
("Charlie" "is" "furry" "+")
((((triple5) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is rough.[(triple3)] Charlie is blue.[(triple4)] Charlie is nice.[(triple5)] Charlie is not round.[(triple7)] Charlie is rough.[(triple6)] Erin is furry.[(triple8)] Erin is not round.[(triple9)] Harry is big.[(triple10 OR ((triple13) -> rule2))] Harry is blue.[(triple11 OR ((triple15) -> rule4))] Harry is furry.[(triple12)] Harry is nice.[(triple13)] Harry is rough.[(triple14)] Harry is round.[(triple15)] @1: Anne is big.[(((triple2) -> rule2))] Charlie is big.[(((triple5) -> rule2))] @2: Charlie is not furry.[(((((triple5) -> rule2) triple7) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is not round.
("Charlie" "is" "round" "-")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is not round.
("Erin" "is" "round" "-")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple13) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((triple15) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple5) -> (rule2 % int2)) triple7) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2