Anne is big. Anne is cold. Anne is rough. Anne is young. Charlie is big. Charlie is nice. Charlie is young. Erin is furry. Erin is rough. Erin is young. Harry is big. Harry is cold. Harry is nice. Harry is rough. Harry is round. Harry is young. All furry, nice people are round. If someone is furry and nice then they are big. If Harry is round and Harry is cold then Harry is young. All furry people are big. All big people are nice. If someone is furry and young then they are cold. If someone is furry and cold then they are rough. If someone is furry and nice then they are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
All furry, nice people are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and nice then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Harry is round and Harry is cold then Harry is young.
((("Harry" "is" "round" "+") ("Harry" "is" "cold" "+")) -> ("Harry" "is" "young" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and young then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry and cold then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry and nice then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Anne is young.
True
1
proof
[(triple4)]
("Anne" "is" "young" "+")
triple4
Anne is not cold.
False
1
inv-proof
[(triple2)]
("Anne" "is" "cold" "-")
triple2
Erin is big.
True
2
proof
[(((triple8) -> rule4))]
("Erin" "is" "big" "+")
((triple8) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is nice.
True
3
proof
[(((((triple8) -> rule4)) -> rule5))]
("Erin" "is" "nice" "+")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule5))]
("Erin" "is" "nice" "-")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
True
5
proof
[(((triple8 ((((triple8) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "round" "+")
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not round.
False
5
inv-proof
[(((triple8 ((((triple8) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "round" "-")
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Anne is round.
Unknown
rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is rough.[(triple3)] Anne is young.[(triple4)] Charlie is big.[(triple5)] Charlie is nice.[(triple6 OR ((triple5) -> rule5))] Charlie is young.[(triple7)] Erin is furry.[(triple8)] Erin is rough.[(triple9 OR ((triple8 ((triple8 triple10) -> rule6)) -> rule7) OR ((triple8 ((triple8 ((((triple8) -> rule4)) -> rule5)) -> rule8)) -> rule7))] Erin is young.[(triple10)] Harry is big.[(triple11)] Harry is cold.[(triple12)] Harry is nice.[(triple13 OR ((triple11) -> rule5))] Harry is rough.[(triple14)] Harry is round.[(triple15)] Harry is young.[(triple16 OR ((triple15 triple12) -> rule3))] @1: Anne is nice.[(((triple1) -> rule5))] Erin is big.[(((triple8) -> rule4))] Erin is cold.[(((triple8 triple10) -> rule6) OR ((triple8 ((((triple8) -> rule4)) -> rule5)) -> rule8))] @2: Erin is nice.[(((((triple8) -> rule4)) -> rule5))] @3: Erin is round.[(((triple8 ((((triple8) -> rule4)) -> rule5)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
((triple5) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
((triple8 ((triple8 triple10) -> (rule6 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple8 ((triple8 ((((triple8) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
((triple11) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple15 triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple8) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple8 triple10) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3