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